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 (computer scientist)|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 =  | discontinued = | latest release version = 4.5.1 | latest release date = 2020-07-15 | latest preview version = | latest preview date =  | 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 =  | 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 (computer scientist)|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 (computer scientist)| 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 (computer scientist)| 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]]