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