NOTE: Many of the theorems we have proved assume you have installed the Prover9 version of June 2006B ("LADR-June-2006B"). Our files may not work with later versions (e.g., they will not work with the August-2006A version or later, since the flags we set for the June-2006B version are no longer valid in the August-2006A version). However, in some cases, we have added a link to input and output files that work with later versions of Prover9.
You can download a gzipped tarball of the June 2006B version of PROVER9 by following one of these links:
You will need to expand the Unix/Mac archive and compile the program yourself; the Windows version comes only as a binary, without sources.
Assuming that you have installed the above version of PROVER9, you can download the input and output files linked in below and process them. The standard command-line syntax for running PROVER9 is:
prover9 < theorem.in
or, if you want to append PROVER9's output to a file:
prover9 < theorem.in > theorem.out
If you need further help in running PROVER9, you can consult the manual that goes with the June 2006B version of PROVER9, which can be viewed at the following location:
Similarly, one can use MACE4 to find models of the axioms used in the proof of each theorem. This provides a finite verification of the consistency of the axioms and definitions. The standard command-line syntax for running MACE4 is (unless otherwise noted):
mace4 -c -N 8 -p 1 < model.in
or, if you want to append MACE4's output to a file,
mace4 -c -N 8 -p 1 < model.in > model.out
You can download a gzipped tarball of PROVER9 versions *after* the June 2006B by following this links:
You will need to expand the Unix/Mac archive and compile the program yourself; the Windows version comes only as a binary, without sources.
You can download a graphical front-end to Prover9 and Mace from here:
http://www.cs.unm.edu/~mccune/mace4/gui/v05.html
This is a very easy way to get started with Prover9 and Mace. You can copy the assumptions and goals from our input files and paste them into the appropriate windows in the graphical application. (1) Copy the assumptions but omit the "formulas(sos)." and "end_of_list." (Commented lines are allowed and will be ignored.) (2) Copy the un-negated version of the theorem to be proved (i.e., the goal) into the Goal sub-window. Start Prover9 with the upper Start button. When you run Mace using the lower Start button, be sure to scroll the any model it outputs to the "Cooked" format, which is much easier to read.