Prover9 Manual Version June-2006

Prover9 Manual

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 clauses or formulas representing the problem. See the Section Clauses and Formulas.

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

Related Programs

Several useful 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.

Other Theorem Provers

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.