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.