vampire (theorem Provers)

Vampire (theorem provers)
From Wikipedia, the free encyclopedia
Jump to: navigation, search
This article contains too much jargon and may need simplification or further explanation. Please discuss this issue on the talk page, and/or remove or explain jargon terms used in the article. Editing help is available. (December 2009)

Vampire is an automatic theorem provers for first-order classical logic developed in the Computer Science Department of the University of Manchester by Prof. Andrei Voronkov previously together with Dr. Alexander Riazanov. It has won the "world cup for theorem provers" (the CADE ATP System Competition) in the most prestigious CNF (MIX) division for ten years (1999, 2001–2009).
Its kernel implements the calculi of ordered binary resolution and superposition for handling equality. The splitting rule and negative equality splitting are simulated by the introduction of new predicate definitions and dynamic folding of such definitions. A number of standard redundancy criteria and simplification techniques are used for pruning the search space: subsumption, tautology deletion (optionally modulo commutativity), subsumption resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of substitution terms. The reduction orderings used are the standard Knuth-Bendix ordering and a special non-recursive version of the 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 specialization is used to accelerate some costly operations, e.g., checks of ordering constraints.
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 classifies 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 classification phase and the refutation of the CNF.
Sources and executables of the system can be obtained from the competition archive of CASC, however Vampire is not open source and no modification, distribution, or even use of Vampire is permitted without a license. A somewhat outdated version is available under LGPL here, as part of Sigma KEE.