Introduction

Prover9 is a resolution/paramodulation automated theorem prover for first-order and equational logic. Prover9 is a successor of the Otter Prover [McCune-Otter33].

Getting Started

Prover9 has a fully automatic mode in which the user simply gives it formulas representing the problem. See the Section Clauses and Formulas.

An good way to learn about Prover9 is to browse and study the example input and output files. Users are encouraged to contribute examples from their own work with Prover9 (and Mace4).

Related Programs

Several programs come bundled with Prover9. The most important is Mace4, which looks for finite models and counterexamples. Mace4 can help avoid wasting time searching for a proof with Prover9 by first finding a counterexample or by first helping to debug logical specifications.

Another useful program is Prooftrans, which can transform proofs found by Prover9 in various ways, including producing more detailed proofs, simplifying the justifications, renumbering the steps, producing proofs in XML, and producing proofs for input to other programs.

Terms of Use

Prover9, Mace4, related programs, and the LADR libraries (with which they were all constructed) are distributed under the terms of the GNU General Public License (v2).

Other Theorem Provers

E is a very good all-around prover.
Waldmeister is a fast prover for equational logic.
Vampire has lately been winning the MIX category of CASC.
Paradox is an excellent program for finding finite models and counterexamples.

Format Conventions for this Manual

Many parts of this manual are displayed in boxes with different background colors.

A display like the following indicates part of an input or output file.

formulas(sos).
  all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y)))).
end_of_list.

formulas(goals).
  all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z)).
end_of_list.

A display like the following indicates a job that is run on a command line, for example, a command to run a Prover9 job.

prover9 -f subset_trans.in > subset_trans.out

A display like the following indicates some output that appears on the computer screen, for example, a message from Prover9.

-------- Proof 1 -------- 
THEOREM PROVED
------ process 3666 exit (max_proofs) ------

Displays like the following contain algorithms.

Simplify clause (c):
    demodulate c
    merge identical literals

A display like the following notes an important difference between Prover9 and Otter.

Prover9's automatic mode is set by default. Otter's automatic mode must be explicitly set.

Next Section: Installation