Prover9 Manual | Version 2009-11A |
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).
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.
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.outA 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 literalsA 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.