Editing Vampire (theorem prover) (section)

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