prooftrans1
Tool for transforming prover9 proofs
Usage
prooftrans [parents_only]
[expand]
[renumber]
[striplabels]
[-f
file]
prooftrans xml
[expand]
[renumber]
[striplabels]
[-f
file]
prooftrans ivy
[renumber]
[-f
file]
prooftrans hints
[-label
label]
[expand]
[striplabels]
[-f
file]
prooftrans tagged
[-f
file]
Overview
This manual page documents briefly the prooftrans command.
prooftrans can extract proofs from prover9(1) output files and transform them in various ways.
Options
A summary of options is included below.
|
Renumber steps. |
|---|---|
|
Simplify justifications by listing only parents. |
|
Expand all steps, turning secondary justifications into explicit steps. |
|
Produce proofs in XML. |
|
Produce proofs for checking by the IVY proof checker. |
|
Produce hints for guiding subsequent searches. |
|
Produce proofs in a structured tagged format. |
-
-label label -
Attach label attributes to the hint clauses consisting of the string label and a sequence number generated by prooftrans.
-
-f file -
Take input from file instead of from standard input.
Releases
6 releases since Debian 5.0 (Lenny); the text changed 1 time.