About Vampire

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: the superposition calculus. This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise an advanced theory in practically valuable tools.

Vampire is a theorem prover, that is, a system able to prove theorems — although now it can do much more! Its main focus is in proving theorems in first-order logic but it can also disprove non-theorems and build finite models, as well as reasoning in combinations of theories, such as arithmetic, arrays, and datatypes, and increasingly in the presence of higher-order logic. The development of Vampire began in 1994 and has survived a number of rewrites (see history).

Features