A Higher-Order Vampire (Short Paper)
Ahmed Bhayat, Martin Suda

TL;DR
This paper discusses recent developments in Vampire theorem prover's support for higher-order reasoning, including new theoretical ideas, implementation details, and empirical performance results.
Contribution
It introduces a reworked approach to higher-order reasoning in Vampire with new theoretical concepts, implementation, and strategy scheduling.
Findings
Implementation of higher-order calculus in Vampire
Empirical performance statistics show improvements
Discussion of ongoing theoretical development
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsGothic Literature and Media Analysis · Crime and Detective Fiction Studies · Sexuality, Behavior, and Technology
