A Higher-Order Vampire (Short Paper)
arXiv:2407.05208
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.
8 pages + references + 1 appendix, accepted to IJCAR 2024 (without the appendix)