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): This site has been replaced by a newer release of Prover9 but is being kept for historical reasons.

Download One of the Following:

LADR: Command-line versions of Prover9, Mace4, and other programs
The GUI: Prover9 and Mace4 with a Graphical User Interface
Update (2024-feb-02): See MacGUI for information on getting the GUI to run on more recent versions of macOS.

Other Useful Links

Manual and Examples
Help! If you have questions about Prover9/Mace4/LADR, e-mail the author.
Citing the programs in your publications
Double-check your Prover9 Proofs with Ivy
Let us know if you would like to be on the email list for notification of updates, bugs, etc.

You should ignore any rumors that Prover9 is part of a bigger plan.

This material is based upon work supported by the National Science Foundation under Grant No. 0708218.

Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.