Prover9 Manual Version June-2006

Prover9 Input Files

Prover9 takes its input from one or more (usually one) files. If there is more than one input file, lists of objects (clauses, formulas, weighting rules, etc.) cannot be split across more than one file. The page Running Prover9 shows how to specify the files in the commands to run Prover9.

The difference between clauses and formulas is a frequent source of confusion for Prover9 (and Otter) users. The page Clauses and Formulas describes the differences. For now, simply note that clauses and formulas are different types of objects; either or both can be used to state the logical specification of the problem.

Comments and Whitespace

Everything from the first % (percent sign) on a line through the end of the line is treated as a comment and ignored. In particular, comments are not echoed to the output file. (Clauses can have label attributes which can serve as different kind of comment which does appear in the output file.)

Whitespace (spaces, newlines, tabs, etc.) is optional in most situations. The important exception is that whitespace is required around some operations in clauses and formulas (see the page Clauses and Formulas).

A Simple Example

The most basic kind of input file consists of list of clauses named "sos" representing the negation of the conjecture, as in the following example.
clauses(sos).   % clauses to be placed in the sos list
  -man(x) | mortal(x).
  man(george).
  -mortal(george).
end_of_list.
Prover9 will take the clauses, use its automatic mode to decide on the inference rules, and then search for a refutation.

The preceding example can also be stated in a positive form by usine the goals list, as follows.

clauses(sos).   % clauses to be placed in the sos list
  -man(x) | mortal(x).
  man(george).
end_of_list.

clauses(goals).  % positive units to be negated and placed in the sos list
  mortal(george).
end_of_list.

A third way of stating the conjecture uses formulas instead of clauses. Note that a clause without variables is also a formula, with the same meaning.

formulas(sos).   % formulas to be translated to clauses and placed in the sos list
  all x (man(x) -> mortal(x)).
  man(george).
end_of_list.

formulas(goals).  % formulas to be negated, translated to clauses, placed in sos
  mortal(george).
end_of_list.
The searches for the the three preceding inputs should all be similar, but they are not guaranteed to be identical, because clause order and symbols may be different.

Types of Input

Prover9 input consists of lists of objects (clauses, formulas, or terms) and commands.

Lists of Objects

Lists of objects start with a type (clauses, formulas, or terms) and name (sos, goals, weights, etc.), and end with end_of_list. The following display show an example of each type of accepted list, with one object in each list.
clauses(sos).           p(x).     end_of_list.   % heavily used
clauses(goals).         p(x).     end_of_list.   % must be positive units (see Goals)
clauses(usable).        p(x).     end_of_list.   % seldom used
clauses(demodulators).  f(x)=x.   end_of_list.   % seldom used, must be equalities
clauses(hints).         p(x).     end_of_list.   % should be used more often  (see Hints)

formulas(sos).          all x p(x).   end_of_list.   % heavily used
formulas(goals).        all x p(x).   end_of_list.   % at most one formula (see Goals)
formulas(usable).       all x p(x).   end_of_list.   % seldom used

terms(weights).         weight(a) = 10.                         end_of_list. % see Weighting
terms(kb_weights).      a = 3.                                  end_of_list. % see Term Ordering
terms(actions).         given = 100 -> set(print_kept).         end_of_list. % see Actions
terms(interpretations). interpretation(2,[],[relation(p,[1])]). end_of_list. % see Semantics
If the input contains morethan one list of a particular type/name, the lists are simply concatenated by Prover9 as they are read.

Commands

Eight types of command are accepted. Here is an example of each.
op(400, infix_right, [+, --]). % declare parse precedence and type (see Clauses and Formulas)

set(fof_reduction).            % set a flag

clear(auto_inference).         % clear a flag

assign(sos_limit, 20000).      % integer parameter

assign(stats, some).           % string parameter

assoc_comm(*).                 % not currently used

commutative(g).                % not currently used

lex([0,1,a,b,f,g,*,+]).        % symbol precedence (see Term Ordering)

skolem([a,b,f,g]).             % declare symbols to be Skolem function (rarely used)

Order of Commands and Lists of Objects

For the most part, the order of things in the input file(s) is irrelevant. For example, commands can usually be mixed with lists of objects. The situations in which order matters are listed here. Note that changing the order of clauses or formulas within a list, changing the order of literals in a clause, or changing the order of subformulas in a formula can change the search, occasionally in profound ways.