A Higher-Order Vampire (Short Paper)
Logic in Computer Science
2024-07-09 v1
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.
Keywords
Cite
@article{arxiv.2407.05208,
title = {A Higher-Order Vampire (Short Paper)},
author = {Ahmed Bhayat and Martin Suda},
journal= {arXiv preprint arXiv:2407.05208},
year = {2024}
}
Comments
8 pages + references + 1 appendix, accepted to IJCAR 2024 (without the appendix)