·
4 commits
to master
since this release
A comprehensive modernization of William McCune's codebase, faithful to his documented intentions. The TPTP input support in particular fulfills a goal he left written in the manual. His underlying algorithms are unchanged. Prover9 is a resolution and paramodulation-based theorem prover for first-order and equational logic, and Mace4 searches for finite counterexamples. Both were developed by William McCune at Argonne National Laboratory, and together proved instrumental in the solution of the Robbins Problem and numerous other open questions in algebra.
To compile run:
tar xzf Prover9-LADR-2026-4E.tar.gz
cd Prover9-LADR-2026-4E
make all
For statically linked binaries on Linux (portable across glibc versions):
make all STATIC=1