PROOFTRANS(1) General Commands Manual PROOFTRANS(1)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)
Check Out this Related Man Page
PROVER9(1) General Commands Manual PROVER9(1)NAME
prover9 - resolution/paramodulation theorem prover
SYNOPSIS
prover9 [options] < input-file > output-file
prover9 [options] -f input-file > output-file
DESCRIPTION
This manual page documents briefly the prover9 command.
prover9 is an automated theorem prover for first-order and equational logic. It is a successor of the otter(1) prover. prover9 uses the
inference techniques of ordered resolution and paramodulation with literal selection.
OPTIONS
A summary of options is included below.
-h View a list of command-line options.
-x Enables an experimental enhanced auto-mode. For more information consult the prover9 manual.
-p Fully parenthesize output.
-t n Constrain the search to last about n seconds. For UNIX-like systems, the `user CPU' time is used.
-f file
Take input from file instead of from standard input.
SEE ALSO mace4(1), otter(1).
On Debian systems, the manual is found in the prover9-doc package, at /usr/share/doc/prover9-doc/manual/index.html.
AUTHOR
prover9 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).
August 12, 2007 PROVER9(1)
I have a file with the following format, i need to change de field9 each 3 rows to renumber field9 with gpo1, gpo2, gpo3.
I need to use awk
Original file
field1 field2 field3 field4 field5 field6 field7 field8 gpo3
field1 field2 field3 field4 field5 ... (3 Replies)
Hello, I need some help to correct my algorithm steps to sum a number. I am confused... please input some steps
Example:
Let's say a number 5.
Now we can get a list of numbers: 1, 2, 3, 4 (less than 5 in sorted order).
so the sum could be: 1+4; 2+3 ( 1+1+1+1+1 or 1+2+2 is not a solution).
... (1 Reply)
Hello,
I have some files in a directory and a short list of strings. I want to loop through the files and remove lines containing the string and renumber.
There are some issues. The first is the strings that can contain troublesome characters like single quotes and parenthesis. Here is one... (12 Replies)