A Higher-Order Vampire (Short Paper)

EasyChair Preprint no. 13125

Abstract

The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are still under development, so we discuss them at a high level in this paper. We also describe the implementation of the calculus in the Vampire theorem prover, the strategy schedule construction, and several empirical performance statistics.

Keyphrases: higher-order, Strategy Scheduling, superposition, Vampire

@Booklet{EasyChair:13125,
  author = {Ahmed Bhayat and Martin Suda},
  title = {A Higher-Order Vampire (Short Paper)},
  howpublished = {EasyChair Preprint no. 13125},

  year = {EasyChair, 2024}}