prover9 ☆
« Back to VersTracker
Description:
Automated theorem prover for first-order and equational logic
Type: Formula  |  Latest Version: 2009-11A@0  |  Tracked Since: Dec 28, 2025
Links: Homepage  |  formulae.brew.sh
Category: Developer tools
Tags: theorem-prover logic formal-verification research mathematics
Install: brew install prover9
About:
Prover9 is an automated theorem prover for first-order and equational logic. It is the successor to the popular Otter prover, providing a powerful engine for proving mathematical conjectures and logical statements. The tool is often used in conjunction with Mace4, which searches for counterexamples to refutations.
Key Features:
  • Automated proof search engine for first-order logic
  • Supports equational logic and clause logic
  • Integrates seamlessly with the Mace4 model finder
  • Input syntax based on standard logical notation
Use Cases:
  • Verifying mathematical theorems and logical proofs
  • Finding counterexamples to logical conjectures
  • Research in automated reasoning and artificial intelligence
Alternatives:
  • E Theorem Prover – E is a purely equational theorem prover, while Prover9 handles first-order logic with equality.
  • Vampire – Vampire is a high-performance first-order prover often used in competitions, whereas Prover9 is known for its integration with Mace4 for model finding.
Version History
Detected Version Rev Change Commit
Sep 15, 2025 7:33am 2009-11A 0 VERSION_BUMP b1092948
Sep 13, 2024 6:03pm 2009-11A 0 VERSION_BUMP 7376455b
Sep 12, 2024 10:42pm 2009-11A 0 VERSION_BUMP 722eef74
« Back to VersTracker  |  Browse Packages  |  About