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.)
Prover9 for Unix-like Systems (Linux, Mac OS X)
For differences between the versions, see the
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.)
- Binaries of Prover9, Mace4, and several other programs are included.
- Source code is availble in the unix version above.
- You don't need Cygwin on your Windows computer to run the programs.
- These are command-line programs;
a GUI is in the works.
- Unzip the package, and see the README.txt file.
If you have suggestions for improving the Windows version,
let us know.