Vampire is an

automatic theorem prover Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

for

first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...

classical logic Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this class ...

developed in the Department of Computer Science at the

University of Manchester , mottoeng = Knowledge, Wisdom, Humanity , established = 2004 – University of Manchester Predecessor institutions: 1956 – UMIST (as university college; university 1994) 1904 – Victoria University of Manchester 1880 – Victoria Univer ...

. Up to Version 3, it was developed by

Andrei Voronkov Andrei Anatolievič Voronkov (born 1959) is a Professor of Formal methods in the Department of Computer Science at the University of Manchester. Education Voronkov was educated at Novosibirsk State University, graduating with a PhD in 1987. Res ...

together with Kryštof Hoder and previously with Alexandre Riazanov. Since Version 4, the development has involved a wider international team including Laura Kovacs, Giles Reger, and Martin Suda. Since 1999 it has won at least 53 trophies in the

CADE ATP System Competition The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organi ...

, the "world cup for theorem provers", including the most prestigious FOF division and the theory-reasoning TFA division.

Background

Vampire's kernel implements the calculi of ordered

binary resolution In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically ...

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 algorithm splitting is also supported. A number of standard redundancy criteria and simplification techniques are used for pruning the search space: tautology deletion,

subsumption Subsumption may refer to: * A minor premise in symbolic logic (see syllogism) * The Liskov substitution principle in object-oriented programming * Subtyping in programming language theory * Subsumption architecture in robotics * A 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, 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 phase and the refutation of the conjunctive normal form. Along with proving theorems, Vampire has other related functionalities such as generating interpolants.

Executable In computing, executable code, an executable file, or an executable program, sometimes simply referred to as an executable or binary, causes a computer "to perform indicated tasks according to encoded instruction (computer science), instructi ...

s can be obtained from the system website. As of November 2020, Vampire is released under modified version of the BSD 3-clause licence which explicitly permits commercial use. Previous versions were available under a proprietary non-commercial licence.

References

External links

* Theorem proving software systems Department of Computer Science, University of Manchester {{logic-stub