Vampire theorem prover

Vampire theorem prover is a computer program that uses the superposition calculus to prove theorems in first-order logic, as well as disprove non-theorems and build finite models. It can reason in combinations of theories, including arithmetic, arrays, and datatypes, and supports (inductive) reasoning over algebraic data types. Developed since 1994, Vampire has been used in various applications such as software verification, hardware design, and knowledge representation.