Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Prover9 and Mace4

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.

Pick One of the Following:

Download Prover9-Mace4 (Prover9 and Mace4 with a Graphical User Interface)
Download LADR (command-line versions of Prover9 and Mace4)

Manual and Examples

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..

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.