prover9 Man page

PROVER9(1) General Commands Manual PROVER9(1)


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 lit‐
eral 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 informa‐
tion 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, otter(1).
On Debian systems, the manual is found in the prover9-doc package, at


prover9 was written by William McCune

This manual page was written by Peter Collingbourne ,
for the Debian project (but may be used by others).

August 12, 2007 PROVER9(1)