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