sourCEntral - mobile manpages

pdf

PROOFTRANS

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 AT cs DOT unm DOT edu>

This manual page was written by Peter Collingbourne <pcc03 AT doc DOT ic DOT ac DOT uk>, for the Debian project (but may be used by others).

pdf