# The Vampire and the FOOL

arXiv: https://arxiv.org/abs/1510.04821 · HTML: https://mlsanity.com/paper/1510.04821/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Oct 2015.

## Built on by (most cited first, 1 of 1)

- [When Agda met Vampire](https://mlsanity.com/paper/2602.18844/) (2026)

## Abstract (arXiv)

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.