PROOFTRANS(1) General Commands Manual PROOFTRANS(1)
prooftrans – tool for transforming Prover9 proofs
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]
This manual page documents briefly the prooftrans command.
prooftrans can extract proofs from prover9 output files and trans‐
form them in various ways.
A summary of options is included below.
Simplify justifications by listing only parents.
expand Expand all steps, turning secondary justifications into explicit
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.
Attach label attributes to the hint clauses consisting of the
string label and a sequence number generated by prooftrans.
Take input from file instead of from standard input.
Full documentation for prooftrans is found in the prover9 manual,
available on Debian systems in the prover9-doc package at
prooftrans was written by William McCune
This manual page was written by Peter Collingbourne
for the Debian project (but may be used by others).
January 20, 2007 PROOFTRANS(1)