Download PDFOpen PDF in browser

A Higher-Order Vampire (Short Paper)

EasyChair Preprint no. 13125

13 pagesDate: April 28, 2024


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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Ahmed Bhayat and Martin Suda},
  title = {A Higher-Order Vampire (Short Paper)},
  howpublished = {EasyChair Preprint no. 13125},

  year = {EasyChair, 2024}}
Download PDFOpen PDF in browser