xenial (1) prooftrans.1.gz

Provided by: prover9_0.0.200911a-2.1_amd64 bug

NAME

       prooftrans - tool for transforming Prover9 proofs

SYNOPSIS

       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]

DESCRIPTION

       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.

AUTHOR

       prooftrans was 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)