The vampire and the FOOL

Evgenii Kotelnikov; Laura Kovács; Giles Reger; Andrei Voronkov

doi:10.1145/2854065.2854071

The vampire and the FOOL

Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov

Chalmers University of Technology

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016
Place of Publication	New York
Publisher	Association for Computing Machinery
Pages	37-48
Number of pages	12
ISBN (Print)	9781450341271
DOIs	https://doi.org/10.1145/2854065.2854071
Publication status	Published - 18 Jan 2016
Event	5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016 - St. Petersburg, United States Duration: 18 Jan 2016 → 19 Jan 2016

Conference

Conference	5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016
Country/Territory	United States
City	St. Petersburg
Period	18/01/16 → 19/01/16

Keywords

Automated theorem proving
First-order logic
Program analysis
Program verification
TPTP
Vampire

Access to Document

10.1145/2854065.2854071

Cite this

@inproceedings{9ef0927134c74cbda2e31c0620797526,

title = "The vampire and the FOOL",

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 = "Automated theorem proving, First-order logic, Program analysis, Program verification, TPTP, Vampire",

author = "Evgenii Kotelnikov and Laura Kov{\'a}cs and Giles Reger and Andrei Voronkov",

year = "2016",

month = jan,

day = "18",

doi = "10.1145/2854065.2854071",

language = "English",

isbn = "9781450341271",

pages = "37--48",

booktitle = "CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016",

publisher = "Association for Computing Machinery",

address = "United States",

note = "5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016 ; Conference date: 18-01-2016 Through 19-01-2016",

}

Kotelnikov, E, Kovács, L, Reger, G & Voronkov, A 2016, The vampire and the FOOL. in CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016. Association for Computing Machinery, New York, pp. 37-48, 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, St. Petersburg, United States, 18/01/16. https://doi.org/10.1145/2854065.2854071

TY - GEN

T1 - The vampire and the FOOL

AU - Kotelnikov, Evgenii

AU - Kovács, Laura

AU - Reger, Giles

AU - Voronkov, Andrei

PY - 2016/1/18

Y1 - 2016/1/18

N2 - 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.

AB - 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.

KW - Automated theorem proving

KW - First-order logic

KW - Program analysis

KW - Program verification

KW - TPTP

KW - Vampire

UR - http://www.scopus.com/inward/record.url?scp=84966552213&partnerID=8YFLogxK

U2 - 10.1145/2854065.2854071

DO - 10.1145/2854065.2854071

M3 - Conference contribution

AN - SCOPUS:84966552213

SN - 9781450341271

SP - 37

EP - 48

BT - CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016

PB - Association for Computing Machinery

CY - New York

T2 - 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016

Y2 - 18 January 2016 through 19 January 2016

ER -

The vampire and the FOOL

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this