prover9 − resolution/paramodulation theorem prover
prover9 [options] < input-file > output-file
prover9 [options] −f input-file > output-file
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.
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.
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.
prover9 was written by William McCune <mccune AT cs DOT unm DOT edu>
This manual page was written by Peter Collingbourne <pcc03 AT doc DOT ic DOT ac DOT uk>, for the Debian project (but may be used by others).