Editing Vampire (theorem prover)

{{Use dmy dates|date=April 2022}}
{{Multiple issues|
{{primary sources|date=May 2018}}
{{Technical|date=December 2009}}
}}

{{Infobox software
| name = Vampire Theorem Prover
| title = 
| logo = 
| logo caption = 
| screenshot = 
| caption = 
| collapsible = 
| author = [[Andrei Voronkov]]<ref>{{cite web|url=https://vprover.github.io/history.html|title=History|website=vprover.github.io|access-date=2018-05-24}}</ref>
| developer = Vampire team
| released = <!-- {{Start date|YYYY|MM|DD|df=yes/no}} -->
| discontinued = 
| latest release version = 4.5.1
| latest release date = 2020-07-15
| latest preview version = 
| latest preview date = <!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| programming language = [[C++]]
| operating system = 
| platform = 
| size = 
| language = Vampire Modified [[BSD Licence]]<ref>{{cite web|url=https://vprover.github.io/licence.html|title=Vampire Licence (Modified BSD)|website=vprover.github.io|access-date=2022-11-02}}</ref>
| language count = <!-- DO NOT include this parameter unless you know what it does -->
| language footnote = 
| genre = [[Automated theorem proving]]
| license = 
| website = {{URL|vprover.github.io/}}
| alexa = 
| standard = 
| AsOf = 
}}
'''Vampire''' is an [[Automated theorem proving|automatic theorem prover]] for [[First-order logic|first-order]] [[classical logic]] developed in the [[Department of Computer Science, University of Manchester|Department of Computer Science]] at the [[University of Manchester]]. Up to Version 3, it was developed by [[Andrei Voronkov]] 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 "world cup for theorem provers", including the most prestigious FOF division and the theory-reasoning TFA division.<ref name="riaznov">{{Cite journal | last1 = Riazanov | first1 = A. | last2 = Voronkov | first2 = A. | author-link2 = Andrei Voronkov| title = The design and implementation of VAMPIRE | journal = AI Communications | volume = 15| number = 2–3/2002 | pages = 91–110 | year = 2002 | issn = 0921-7126}}</ref><ref>{{Cite journal | last1 = Voronkov | first1 = A. | author-link1 = Andrei Voronkov| title = The anatomy of vampire | doi = 10.1007/BF00881918 | journal = [[Journal of Automated Reasoning]] | volume = 15 | issue = 2 | pages = 237–265 | year = 1995 | s2cid = 1541122 }}</ref>

==Background==
Vampire's [[kernel (operating system)|kernel]] implements the calculi of ordered [[binary resolution]] and [[Superposition calculus|superposition]] (for handling equality). The splitting rule and negative equality splitting can be simulated by the introduction of new [[predicate (logic)|predicate]] definitions and dynamic folding of such definitions. A [[DPLL algorithm|DPLL-style algorithm]] splitting is also supported. A number of standard redundancy criteria and simplification techniques are used for pruning the search space:  [[tautology (logic)|tautology]] deletion, [[Hierarchy#Subsumptive containment hierarchy|subsumption]] resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of [[substitution (logic)|substitution]] terms. 
The reduction ordering on [[term (logic)|term]]s is the standard [[Knuth–Bendix completion algorithm|Knuth–Bendix ordering]].

A number of efficient [[term indexing|indexing]] techniques are used to implement all major operations on sets of terms and [[clause (logic)|clause]]s. [[Run-time algorithm specialisation]] is used to accelerate forward matching.

Although the kernel of the system works only with [[conjunctive normal form]]s, the preprocessor component accepts a problem in the full first-order logic syntax, {{not a typo|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 {{not a typo|clausification}} phase and the refutation of the [[conjunctive normal form]].

Along with proving theorems, Vampire has other related functionalities such as generating [[Craig interpolation|interpolants]].

[[Executable]]s can be obtained from the system website.<ref>{{cite web|url=https://vprover.github.io/|title=Vampire|website=vprover.github.io|access-date=2022-11-02}}</ref> 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==
{{reflist}}

==External links==
*{{Official website}}

[[Category:Theorem proving software systems]]
[[Category:Department of Computer Science, University of Manchester]]
[[Category:Free software programmed in C++]]
[[Category:Software using the BSD license]]


{{Logic-stub}}
{{Free-software-stub}}