Prover9 Manual |  | Version 2009-02A

# 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