×

zbMATH — the first resource for mathematics

The design and implementation of VAMPIRE. (English) Zbl 1021.68082
Summary: We describe VAMPIRE: a high-performance theorem prover for first-order logic. As our description is mostly targeted to the developers of such systems and specialists in automated reasoning, it focuses on the design of the system and some key implementation features. We also analyze the performance of the prover at CASC-JC.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
VAMPIRE; OTTER; TPTP
PDF BibTeX Cite