Vampire is an automatic theorem prover for first-order

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 c ...

developed in the

Department of Computer Science Computer science is the study of computation, information, and automation. Computer science spans theoretical disciplines (such as algorithms, theory of computation, and information theory) to applied disciplines (including the design and ...

at the

University of Manchester The University of Manchester is a public university, public research university in Manchester, England. The main campus is south of Manchester city centre, Manchester City Centre on Wilmslow Road, Oxford Road. The University of Manchester is c ...

. 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, University of Manchester, Department of Computer Science at the University of Manchester. Education Voronkov was educated at Novosibir ...

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 an annual competition of fully automated theorem provers for classical logic Competition CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated ...

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

Background

Vampire's

kernel Kernel may refer to: Computing * Kernel (operating system), the central component of most operating systems * Kernel (image processing), a matrix used for image convolution * Compute kernel, in GPGPU programming * Kernel method, in machine learnin ...

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 In mathematics, a linear combination or superposition is an expression constructed from a set of terms by multiplying each term by a constant and adding the results (e.g. a linear combination of ''x'' and ''y'' would be any expression of the form ...

(for handling equality). The splitting rule and negative equality splitting can be simulated by the introduction of new

predicate Predicate or predication may refer to: * Predicate (grammar), in linguistics * Predication (philosophy) * several closely related uses in mathematics and formal logic: **Predicate (mathematical logic) **Propositional function **Finitary relation, o ...

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 Substitution may refer to: Arts and media *Substitution (poetry), a variation in poetic scansion * Substitution (theatre), an acting methodology Music *Chord substitution, swapping one chord for a related one within a chord progression *Tritone ...

terms. The reduction ordering on terms is the standard Knuth–Bendix ordering. A number of efficient indexing techniques are used to implement all major operations on sets of terms and

clause In language, a clause is a Constituent (linguistics), constituent or Phrase (grammar), phrase that comprises a semantic predicand (expressed or not) and a semantic Predicate (grammar), predicate. A typical clause consists of a subject (grammar), ...

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. The methodology originates in the field of automated theorem proving and, more specifically, in ...

is used to accelerate forward matching. Although the kernel of the system works only with

conjunctive normal form In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. In au ...

s, 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

. Along with proving theorems, Vampire has other related functionalities such as generating interpolants.

Executable In computer science, 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), in ...

s can be obtained from the system website. As of November 2020, Vampire is released under a modified version of the BSD 3-clause licence that 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 Free software programmed in C++ Software using the BSD license {{Free-software-stub