.TH PROOFTRANS 1 "January 20, 2007"
.SH NAME
prooftrans - tool for transforming Prover9 proofs
.SH SYNOPSIS
.B prooftrans
.RI [ parents_only ]
.RI [ expand ]
.RI [ renumber ]
.RI [ striplabels ]
[\fI-f file\fP]
.br
.B prooftrans
xml
.RI [ expand ]
.RI [ renumber ]
.RI [ striplabels ]
[\fI-f file\fP]
.br
.B prooftrans
ivy
.RI [ renumber ]
[\fI-f file\fP]
.br
.B prooftrans
hints
[\fI-label label\fP]
.RI [ expand ]
.RI [ striplabels ]
[\fI-f file\fP]
.br
.B prooftrans
tagged
[\fI-f file\fP]
.SH DESCRIPTION
This manual page documents briefly the
.B prooftrans
command.
.PP
\fBprooftrans\fP can extract proofs from
.BR prover9 (1)
output files and transform them in various ways.

.SH OPTIONS
A summary of options is included below.
.TP
.B renumber
Renumber steps.
.TP
.B parents_only
Simplify justifications by listing only parents.
.TP
.B expand
Expand all steps, turning secondary justifications into explicit steps.
.TP
.B xml
Produce proofs in XML.
.TP
.B ivy
Produce proofs for checking by the IVY proof checker.
.TP
.B hints
Produce hints for guiding subsequent searches.
.TP
.B tagged
Produce proofs in a structured tagged format.
.TP
.B \-label \fIlabel\fP
Attach label attributes to the hint clauses consisting of the string \fIlabel\fP and a sequence number generated by prooftrans.
.TP
.B \-f \fIfile
Take input from \fIfile\fP instead of from standard input.
.SH SEE ALSO
.BR prover9 (1).
.br
Full documentation for \fBprooftrans\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
.SH AUTHOR
\fBprooftrans\fP was written by William McCune <mccune@cs.unm.edu>
.PP
This manual page was written by Peter Collingbourne <peter@pcc.me.uk>,
for the Debian project (but may be used by others).