index.html

---
title: Vampire
layout: default
---

<p>
Automatic theorem proving has a number of important applications, such as software verification, hardware verification, 
  hardware design, knowledge representation and reasoning, the Semantic Web, algebra, and proving theorems in mathematics. 
Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in 
  computer science.
This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise 
  an advanced theory in practically valuable tools.
</p>

<p>
Vampire is a theorem prover, that is, a system able to prove theorems &mdash; although now it can do much more! 
Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of <em>theories</em>, such as arithmetic, arrays, and datatypes, and with higher-order logic. 
The development of Vampire began in 1994 and has survived a number of rewritings (see <a href="https://vprover.github.io/history.html">history</a>). 
</p>

<p><b>NEW LICENCE!</b> We are very pleased to announce that Vampire is now available under a <a href="https://vprover.github.io/licence.html">BSD 3-Clause licence</a>, allowing (free) industrial and academic usage. 
  It would be great to hear from you if you are making use of this new licence within your work. Please join our <a href="https://groups.google.com/g/vprover?pli=1"> very low-traffic mailing list</a> for updates. 
You may also want to want to use the <a href="https://github.com/vprover/vampire/issues">GitHub Issues</a> page for questions or issues.
</p>

<h3>Features</h3>
<ul>
  <li>Vampire is very fast, as can be judged by <a href="/trophies.html">our awards</a> at the CASC and SMT-COMP comeptitions</li>
  <li>Vampire has an easy to use <i>portfolio mode</i> (see <a href="https://vprover.github.io/usage.html">Usage</a>) that can be run in multicore mode</li>
  <li>Vampire can "pretend to be an SMT solver" in the sense that it accepts SMT-LIB input (see <a href="https://vprover.github.io/usage.html">Usage</a>)  and can effectively reason in combinations of first-order logic and theories, such as integer arithmetic, which makes it useful for reasoning with theories and quantifiers</li>
  <li>Vampire can produce detailed proofs and finite models</li>
  <li>Vampire supports (inductive) reasoning over algebraic data types (finite term algebras)</li>
  <li>Vampire can generate interpolants</li>
</ul>