vampire ☆

« Back to VersTracker

Description:
High-performance theorem prover

Type: Formula | Tracked Since: Jan 19, 2026

Links: Homepage | formulae.brew.sh

Category: Ai ml

Tags: theorem-prover logic formal-verification automated-reasoning research

Install: brew install vampire

About:
Vampire is a high-performance automated theorem prover for first-order logic, designed for proving theorems in mathematics and computer science. It implements superposition calculus and a variety of proof search strategies, making it a leading tool in formal verification and automated reasoning competitions.

Key Features:

Automated theorem proving for first-order logic
Implements superposition calculus and powerful proof search strategies
Highly configurable with multiple scheduling modes
Regularly competes and ranks highly in the CADE ATP System Competition

Use Cases:

Formal verification of hardware and software systems
Automated reasoning in mathematical research and education
Solving logical problems and puzzles in knowledge representation

Alternatives:

E – Another high-performance theorem prover for first-order logic, often a direct competitor in competitions.
Prover9 – An earlier-generation automated theorem prover for first-order logic, less actively developed.

Version History

Detected	Version	Rev	Change	Commit
Jan 19, 2026 9:31pm		0	META	97308995