The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kov\'acs, Giles Reger, Andrei Voronkov
TL;DR
This paper introduces new features in the Vampire theorem prover, including support for first-order logic with a boolean sort and polymorphic arrays, enhancing expressivity and efficiency for program analysis.
Contribution
The paper presents novel extensions to Vampire, notably support for FOOL and polymorphic arrays, improving reasoning capabilities and performance.
Findings
Enhanced expressivity for reasoning-based program analysis
Improved efficiency in theorem proving tasks
Support for complex logical constructs like if-then-else and let-in
Abstract
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency.
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.