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
Renumber steps.
parents_only
Simplify justifications by listing only parents.
expand
Expand all steps, turning secondary justifications into explicit steps.
xml
Produce proofs in XML.
ivy
Produce proofs for checking by the IVY proof checker.
hints
Produce hints for guiding subsequent searches.
tagged
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.
SEE ALSO
prover9(1).
Full documentation for prooftrans is found in the prover9 manual, available on Debian systems in the prover9-doc package at /usr/share/doc/prover9-doc/manual/index.html.