Prooftrans

When Prover9 proves a theorem, it sends the proof to its output file in a standard form. The standard form contains, for each step, justifications with enough detail to reconstruct or check the proof without any search.

Prover9 proofs may contain non-clausal assumptions and goals, as well as ordinary clauses. Non-clausal assumptions are translated to clauses, and goals are negated and then translated to clauses. See the proof in following example

prover9 -f subset_trans.in > subset_trans.out

Prooftrans can extract proofs from Prover9 output files and transform them in various ways, including the following.

No transformation,
renumber steps,
simplify justifications,
expand all steps, turning secondary justifications into explicit steps,
produce proofs in XML,
produce proofs for checking by the IVY proof checker, and
produce hints for guiding subsequent searches.

Prooftrans is part of the LADR/Prover9/Mace4 package. When the package is installed, the Prooftrans program should be in the same directory as Prover9 and Mace4.

Using Prooftrans

The Prover9 output file containing the proof(s) is usually given to Prooftrans with the argument "-f <filename>". If there is no "-f <filename>" argument, Prooftrans takes its input from the standard input.

The arguments that tell Prooftrans what to do with the proof(s) are described in the following sections, using the output file subset_trans.out as a running example.

If there is more than one proof in the file, the transformations will be applied to each proof. The hints transformation collects all of the clauses in the proof(s) into one list of hints. The other transformations produce one proof for each proof in the input file.

Here is a synopsis of the Prooftrans command; the arguments in square brackets are optional.

prooftrans [parents_only] [expand] [renumber] [striplabels] [-f file]
prooftrans xml            [expand] [renumber] [striplabels] [-f file]
prooftrans ivy                     [renumner]               [-f file]
prooftrans hints [-label label] [expand]      [striplabels] [-f file]

Note that more than one transformation can be applied in several cases. The option "striplabels" tells prooftrans to remove all label attributes on clauses.

Unfortunately, the output of Prooftrans usually cannot be used as the input to another Prooftrans job, because Prooftrans expects its input to have specific keywords and standard-form proofs.

No Transformation

If no additional argument is given, Prooftrans simply extracts the proof from the Prover9 output file.

prooftrans -f subset_trans.out > subset_trans.proof1

Renumber the Steps

The argument renumber tells Prooftrans to renumber the steps of each proof consecutively, starting with step 1. The expand, parents_only, and xml transformations can be used with the renumber transformation.

prooftrans renumber -f subset_trans.out > subset_trans.proof2

Simplify Justifications

The argument parents_only tells Prooftrans list only the parents in the justifications, not the details about inference rules or positions. The expand and renumber transformations can be used with the parents_only transformation.

prooftrans parents_only -f subset_trans.out > subset_trans.proof3

Expand Steps

The argument expand tells Prooftrans to produce more detailed proofs in which

all hyper- and UR-resolution steps are replaced with binary resolution steps,
all demodulation sequences are replaced with paramodulation steps, and
all unit deletion simplifications are replaced with resolution steps.

Note to author: this is a bad example, because only one step gets expanded.

prooftrans expand -f subset_trans.out > subset_trans.proof4

Note that when a step is expanded (step 22 in this example), the new steps are identified by appending 'A', 'B', etc. to the number of the original step.

The renumber, parents_only, and hints transformations can be used with the expand transformation.

XML Proofs

The options xml or XML tell Prooftrans to produce proofs in XML. The options expand and renumber can be used with the XML transformation.

prooftrans xml -f subset_trans.out > subset_trans.proof5.xml

The preceding output is displayed by your browser not as XML, but as some transformation of the XML, because the XML refers to an XML stylesheet, telling the browser how to transform the XML into HTML.

To see the XML source, click "View -> Frame Source" (or something like that) in your browser while viewing the proof.

Here is the DTD for Prover9 XML proofs. (If you get an error, click "View -> Page Source".)

IVY Proofs

The options ivy or IVY tell Prooftrans to produce very detailed proofs that can be checked with the Ivy proof checker.

prooftrans ivy -f subset_trans.out > subset_trans.proof6

Ivy proofs have a only 5 types of step: input, propositional, new_symbol, flip, instantiate, resolve, and paramod. The resolve and paramod do not involve unification; instances are generated first as separate steps, and then resolve or paramod are applied to identical atomic formulas or terms.

The Ivy proof checker cannot check steps justified by new_symbol.

Proofs to Hints

The option hints tells Prooftrans to take all of the proofs in the file and produce one list of hints that can be given to Prover9 to guide subsequent searches on related conjectures.

prooftrans hints -f subset_trans.out > subset_trans.proof7

If there is more than one proof in the file, the proofs will probably share many steps. The list of hints that Prooftrans produces will be the union of the steps in the proofs; that is, the duplicate steps will be removed.

The expand transformation can be used with the hints transformation.

The label option tells prooftrans to attach label attributes to the hint clauses. The labels consist of the string given on the command line and a sequence number generated by prooftrans. The user's command shell may require that the label be quoted, and if the the label is not a legal LADR constant, prooftrans will enclose the label in double quotes.

prooftrans hints -label 'job8' -f subset_trans.out > subset_trans.proof8

Next Section: FOF-Prover9