Prover9 is an automated theorem prover for first-order and equational logic developed by William McCune.
Prover9 is the successor of the Otter theorem prover also developed by William McCune.
Resulting proofs can be double-checked by Ivy, a proof-checking tool that has been separately verified using ACL2.
In July 2006 the LADR/Prover9/Mace4 input language made a major change (which also differentiates it from Otter).
The traditional "all men are mortal", "Socrates is a man", prove "Socrates is mortal" can be expressed this way in Prover9: This will be automatically converted into clausal form (which Prover9 also accepts): A proof that the square root of 2 is irrational can be expressed this way:[3]