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).