1PROOFTRANS(1)               General Commands Manual              PROOFTRANS(1)
2
3
4

NAME

6       prooftrans - tool for transforming Prover9 proofs
7

SYNOPSIS

9       prooftrans [parents_only] [expand] [renumber] [striplabels] [-f file]
10       prooftrans xml [expand] [renumber] [striplabels] [-f file]
11       prooftrans ivy [renumber] [-f file]
12       prooftrans hints [-label label] [expand] [striplabels] [-f file]
13

DESCRIPTION

15       This manual page documents briefly the prooftrans command.
16
17       prooftrans  can  extract proofs from prover9(1) output files and trans‐
18       form them in various ways.
19
20

OPTIONS

22       A summary of options is included below.
23
24       renumber
25              Renumber steps.
26
27       parents_only
28              Simplify justifications by listing only parents.
29
30       expand Expand all steps, turning secondary justifications into explicit
31              steps.
32
33       xml    Produce proofs in XML.
34
35       ivy    Produce proofs for checking by the IVY proof checker.
36
37       hints  Produce hints for guiding subsequent searches.
38
39       -label label
40              Attach  label  attributes  to the hint clauses consisting of the
41              string label and a sequence number generated by prooftrans.
42
43       -f file
44              Take input from file instead of from standard input.
45

SEE ALSO

47       prover9(1).
48       Full documentation for prooftrans  is  found  in  the  prover9  manual,
49       available   on   Debian   systems   in   the   prover9-doc  package  at
50       /usr/share/doc/prover9-doc/manual/index.html.
51

AUTHOR

53       prooftrans was written by William McCune <mccune@cs.unm.edu>
54
55       This   manual    page    was    written    by    Peter    Collingbourne
56       <pcc03@doc.ic.ac.uk>,  for  the Debian project (but may be used by oth‐
57       ers).
58
59
60
61                               January 20, 2007                  PROOFTRANS(1)