A Higher-Order Vampire (Short Paper)

EasyChair Preprint 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: Strategy Scheduling, Vampire, higher-order, superposition

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