The Vampire and the FOOL
Logic in Computer Science
2015-12-08 v2
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.
Keywords
Cite
@article{arxiv.1510.04821,
title = {The Vampire and the FOOL},
author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov},
journal= {arXiv preprint arXiv:1510.04821},
year = {2015}
}