prover91
Resolution/paramodulation theorem prover
Usage
prover9 [options]
<
input-file
>
output-file
prover9 [options]
-f
input-file
>
output-file
Overview
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
prover9manual.
-
-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.
Releases
6 releases since Debian 5.0 (Lenny); the text changed 1 time.