2013 | OriginalPaper | Chapter
First-Order Theorem Proving and Vampire
Authors : Laura Kovács, Andrei Voronkov
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In this paper we give a short introduction in first-order theorem proving and the use of the theorem prover
Vampire
. We discuss the superposition calculus and explain the key concepts of saturation and redundancy elimination, present saturation algorithms and preprocessing, and demonstrate how these concepts are implemented in
Vampire
. Further, we also cover more recent topics and features of
Vampire
designed for advanced applications, including satisfiability checking, theory reasoning, interpolation, consequence elimination, and program analysis.