Vampire theorem prover
Encyclopedia
Vampire is an automatic theorem prover
for first-order
classical logic
developed in the Computer Science Department of the University of Manchester
by
Prof. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov. So far it has won the "world cup for theorem provers" (the CADE ATP System Competition
) in the most prestigious CNF (MIX) division eleven times (1999, 2001–2010).
Its kernel implements the calculi of ordered binary resolution and superposition
for handling equality. The splitting rule and negative equality splitting can be simulated by the introduction of new predicate definitions and dynamic folding of such definitions. A DPLL
-style splitting is also supported. A number of standard redundancy criteria and simplification techniques are used for pruning the search space:tautology
deletion, subsumption resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of substitution terms.
The reduction ordering used is the standard Knuth-Bendix ordering.
A number of efficient indexing
techniques are used to implement all major operations on sets of terms and clauses. Run-time algorithm specialisation
is used to accelerate forward matching.
Although the kernel of the system works only with clausal normal forms, the preprocessor component accepts a problem in the full first-order logic syntax, clausifies it and performs a number of useful transformations before passing the result to the kernel. When a theorem is proven, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the CNF.
Along with proving theorems, Vampire has other related functionalities such as generating interpolants
.
Executables can be obtained from the system web vprover.org.
A somewhat outdated version is available under LGPL here,
as part of Sigma KEE
.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
for first-order
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
developed in the Computer Science Department of the University of Manchester
University of Manchester
The University of Manchester is a public research university located in Manchester, United Kingdom. It is a "red brick" university and a member of the Russell Group of research-intensive British universities and the N8 Group...
by
Prof. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov. So far it has won the "world cup for theorem provers" (the CADE ATP System Competition
CADE ATP System Competition
The CADE ATP System Competition is a yearly competition of fully automated theorem provers for classical first order logic. CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated...
) in the most prestigious CNF (MIX) division eleven times (1999, 2001–2010).
Its kernel implements the calculi of ordered binary resolution and superposition
Superposition calculus
The superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
for handling equality. The splitting rule and negative equality splitting can be simulated by the introduction of new predicate definitions and dynamic folding of such definitions. A DPLL
DPLL algorithm
The Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem....
-style splitting is also supported. A number of standard redundancy criteria and simplification techniques are used for pruning the search space:tautology
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
deletion, subsumption resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of substitution terms.
The reduction ordering used is the standard Knuth-Bendix ordering.
A number of efficient indexing
Term indexing
In computer science, term indexing is the task of creating an index of terms and clauses in a collection.Many operations in automatic theorem provers require search in hugecollections of terms and clauses. Such operations typically fall into...
techniques are used to implement all major operations on sets of terms and clauses. Run-time algorithm specialisation
Run-time algorithm specialisation
In computer science, run-time algorithm specialization is a methodology for creating efficient algorithms for costly computation tasks of certain kinds...
is used to accelerate forward matching.
Although the kernel of the system works only with clausal normal forms, the preprocessor component accepts a problem in the full first-order logic syntax, clausifies it and performs a number of useful transformations before passing the result to the kernel. When a theorem is proven, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the CNF.
Along with proving theorems, Vampire has other related functionalities such as generating interpolants
Craig interpolation
In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ then there is a third formula ρ, called an interpolant, such that every nonlogical symbol...
.
Executables can be obtained from the system web vprover.org.
A somewhat outdated version is available under LGPL here,
as part of Sigma KEE
Sigma knowledge engineering environment
In the computer science fields of knowledge engineering and ontology, the Sigma knowledge engineering environment is an open source computer program for the development of formal ontologies. It is designed for use with the Suggested Upper Merged Ontology...
.