Prover9 (and Mace4) Download

Prover9, Mace4, and several related programs come packaged in a system called LADR (Library for Automated Deduction Research).

If you install one of these LADR packages, you will get command-line programs. (The programs are run by typing commands to a command prompt, terminal, or shell.)

A GUI (graphical user interface) called Prover9-Mace4 is also available. (The GUI is self-contained, so there is no need to install one of these LADR packages to use the GUI.)

Manuals and Examples

Prover9 for Unix-like Systems (Linux, Mac OS X)

For differences between the versions, see the Changelog file.

Download the .tar.gz file, unpack it, go to the LADR directory, and "make all".

Prover9 for MS Windows

(This might not be current with the Unix version.)

Prover9, Mace4, and related programs have been compiled under Cygwin in MS Windows. (Cygwin is a unix-like environment for Windows.)



If you have suggestions for improving the Windows version, let us know.