A Higher-Order Vampire (Short Paper)
Ahmed Bhayat, Martin Suda
TL;DR
The paper addresses the challenge of enabling effective higher-order reasoning in Vampire by replacing full higher-order unification with a depth-bounded unification approach that generates negative constraint literals $C_\sigma$ at the depth bound. It introduces a new higher-order superposition calculus parameterized by a selection function and ordering, and integrates an applicative encoding of HOL into rank-1 polymorphic first-order logic for implementation, augmented by a Spider-inspired strategy discovery and scheduling process. The authors report that these contributions led to Vampire achieving first place in the CASC 2023 THF division and demonstrate substantial problem coverage with a final schedule using 278 of 1158 strategies, including probabilistic scheduling benefits at low time limits. They also discuss comparisons to related work (e.g., EP calculus), practical aspects of the implementation, and avenues for future work such as proving refutational completeness and adding further simplifications. The work shows that intertwining higher-order reasoning with unification and a carefully crafted strategy schedule can significantly enhance performance on TH0/TPTP problems and Sledgehammer benchmarks, while highlighting open theoretical questions nonetheless.
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.