1PROVER9(1)                  General Commands Manual                 PROVER9(1)
2
3
4

NAME

6       prover9 - resolution/paramodulation theorem prover
7

SYNOPSIS

9       prover9 [options] < input-file > output-file
10       prover9 [options] -f input-file > output-file
11

DESCRIPTION

13       This manual page documents briefly the prover9 command.
14
15       prover9  is  an automated theorem prover for first-order and equational
16       logic. It is a successor of the  otter(1)  prover.   prover9  uses  the
17       inference techniques of ordered resolution and paramodulation with lit‐
18       eral selection.
19

OPTIONS

21       A summary of options is included below.
22
23       -h     View a list of command-line options.
24
25       -x     Enables an experimental enhanced auto-mode.  For  more  informa‐
26              tion consult the prover9 manual.
27
28       -p     Fully parenthesize output.
29
30       -t n   Constrain  the  search  to  last about n seconds.  For UNIX-like
31              systems, the `user CPU' time is used.
32
33       -f file
34              Take input from file instead of from standard input.
35

SEE ALSO

37       mace4(1), otter(1).
38       On Debian systems, the manual is found in the prover9-doc  package,  at
39       /usr/share/doc/prover9-doc/manual/index.html.
40

AUTHOR

42       prover9 was written by William McCune <mccune@cs.unm.edu>
43
44       This    manual    page    was    written    by    Peter   Collingbourne
45       <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used  by  oth‐
46       ers).
47
48
49
50                                August 12, 2007                     PROVER9(1)
Impressum