-
Notifications
You must be signed in to change notification settings - Fork 1
System Vampire
Andrei Voronkov, Giles Reger, Martin Suda & others (view website below)
Vampire is an automatic theorem prover for first-order logic with extensions to theory-reasoning and higher-order logic. Vampire implements the calculi of ordered binary resolution and superposition for handling equality. It also implements the Inst-gen calculus and a MACE-style finite model builder. Splitting in resolution-based proof search is controlled by the AVATAR architecture which uses a SAT or SMT solver to make splitting decisions. A number of standard redundancy criteria and simplification techniques are used for pruning the search space: subsumption, tautology deletion, subsumption resolution and rewriting by ordered unit equalities. The reduction ordering is the Knuth-Bendix Ordering. Substitution tree and code tree indexes are used to implement all major operations on sets of terms, literals and clauses. Internally, Vampire works only with clausal normal form. Problems in the full first-order logic syntax are clausified during preprocessing. Vampire implements many useful preprocessing transformations including the SinE axiom selection algorithm. When a theorem is proved, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the CNF.
Vampire is developed at the University of Manchester, the TU Wien and the Czech Technical University in Prague.
- Proving
- Model finding
Vampire supports all common TPTP dialects, including FOF, TFF, and THF as well as their rank-1 polymorphic derivatives. Vampire also supports SMT-LIB 2.6.
Vampire follows the SZS reporting standard
Vampire outputs proofs in the TPTP format.
Vampire is written in C/C++.
Vampire may be cited with DOI 10.1007/978-3-642-39799-8_1.
Vampire is included in the Sledgehammer tool of Isabelle/HOL.
Vampire participates in the annual CASC ATP system competition and the annual SMT competition SMT-COMP
Maintained
Kovács, L., Voronkov, A. (2013). First-Order Theorem Proving and Vampire . In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. DOI: https://doi.org/10.1007/978-3-642-39799-8_1