SYNOPSISprooftrans [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]
DESCRIPTIONThis manual page documents briefly the prooftrans command.
prooftrans can extract proofs from prover9(1) output files and transform them in various ways.
OPTIONSA 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.
AUTHORprooftrans was written by William McCune <[email protected]>
This manual page was written by Peter Collingbourne <[email protected]>, for the Debian project (but may be used by others).