Prover9 and Mace4

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

Update (2026-mar-17): In March 2026 Jeffrey P. Machado and Larry Lesyna substantially revised and added new features to Prover9 and Mace4. Their new version is called LADR-2026. LADR-2026 is backwards compatible with LADR-2009, and installation of LADR-2026 is recommended for all Prover9 and Mace4 users. Please visit the site https://prover9.org for documentation download and all other information.

The home page for the older version of Prover9 is available here.