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.

Download One of the Following:

Other Useful Links

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.