Provided by: prover9_0.0.200911a-2.1build1_amd64

**NAME**

prooftrans - tool for transforming Prover9 proofs

**SYNOPSIS**

prooftrans[parents_only] [expand] [renumber] [striplabels] [-ffile]prooftransxml [expand] [renumber] [striplabels] [-ffile]prooftransivy [renumber] [-ffile]prooftranshints [-labellabel] [expand] [striplabels] [-ffile]prooftranstagged [-ffile]

**DESCRIPTION**

This manual page documents briefly theprooftranscommand.prooftranscan extract proofs fromprover9(1) output files and transform them in various ways.

**OPTIONS**

A summary of options is included below.renumberRenumber steps.parents_onlySimplify justifications by listing only parents.expandExpand all steps, turning secondary justifications into explicit steps.xmlProduce proofs in XML.ivyProduce proofs for checking by the IVY proof checker.hintsProduce hints for guiding subsequent searches.taggedProduce proofs in a structured tagged format.-labellabelAttach label attributes to the hint clauses consisting of the stringlabeland a sequence number generated by prooftrans.-ffileTake input fromfileinstead of from standard input.

**SEE** **ALSO**

prover9(1). Full documentation forprooftransis found in theprover9manual, available on Debian systems in theprover9-docpackage at/usr/share/doc/prover9-doc/manual/index.html.

**AUTHOR**

prooftranswas written by William McCune <mccune@cs.unm.edu> This manual page was written by Peter Collingbourne <peter@pcc.me.uk>, for the Debian project (but may be used by others). January 20, 2007 PROOFTRANS(1)