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 (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.

Comments and Whitespace

There are two kinds of comment:

Line comment. If the first '%' (percent sign) on a line is not the start of a block comment ('%BEGIN'), everything from that symbol through the end of the line is ignored.
Block comment. If the parser sees the string '%BEGIN', that is not in a line comment, it will ignore everything up through the next occurrence of 'END%'. Line breaks are irrelevant. If there is no 'END%', the rest of the file is ignored, without causing an error.

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 places. 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.

formulas(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 more natural way by using a non-clausal formula for the man-implies-mortal rule and the goals list for the conclusion, as follows.

formulas(assumptions).   % synonym for formulas(sos).
  man(x) -> mortal(x).   % open formula with free variable x
  man(george).
end_of_list.

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

Prover9 will transform the formulas in this input to the same clauses as in the basic input above before starting the search for a refutation.

In Otter and in earlier versions of Prover9, "clauses" and "formulas" were distinct types of object, and formulas could not have free variables. Now, clauses are a subset of formulas, and Prover9 decides which formulas are non-clausal and takes the appropriate actions to transform them to clauses.

Types of Input

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

Lists of Objects

Lists of objects start with a type (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.

formulas(sos).           p(x).     end_of_list.   % the primary input list
formulas(assumptions).   p(x).     end_of_list.   % synonym for formulas(sos)
formulas(goals).         p(x).     end_of_list.   % some restrictions (see Goals)
formulas(usable).        p(x).     end_of_list.   % seldom used
formulas(demodulators).  f(x)=x.   end_of_list.   % seldom used, must be equalities
formulas(hints).         p(x).     end_of_list.   % should be used more often  (see Hints)

list(weights).         weight(a) = 10.                         end_of_list. % see Weighting
list(kbo_weights).     a = 3.                                  end_of_list. % see Term Ordering
list(actions).         given = 100 -> set(print_kept).         end_of_list. % see Actions
list(interpretations). interpretation(2,[],[relation(p,[1])]). end_of_list. % see Semantics

If the input contains more than one list of a particular type/name, the lists are simply concatenated by Prover9 as they are read.

Commands

Eleven types of command are accepted. Here is an example of each.

op(400, infix_right, ["+", "--"]). % declare parse precedence and type (see Clauses and Formulas)

redeclare(negation, "~"]).         % change the negation symbol (see Clauses and Formulas)

set(print_kept).                   % set a flag

clear(auto_inference).             % clear a flag

assign(max_weight, 40).            % integer parameter

assign(stats, some).               % string parameter

assoc_comm(*).                     % not currently used for Prover9

commutative(g).                    % not currently used for Prover9

predicate_order([=,<=,P,Q).        % predicate symbol precedence (see Term Ordering)

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

lex([0,1,a,b,f,g,*,+]).            % synonym for "function_order"

skolem([a,b,f,g]).                 % declare symbols to be Skolem functions (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.

The op(precedence, type, symbols) commands must occur before any clauses or formulas that contain the affected symbols.
Some of the flags and parameters alter other flags and parameters. The alterations can be undone by placing the appropriate command after the command that alters. The output file clearly shows what happens in these cases.

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 substantial ways.

Conditional Inclusion

Many input files can be used for multiple programs (e.g., Prover9 and Mace4). The following construct says to include the enclosed input for the given program only.

if(program-name).
   ... conditionally-included input ...
end_if.

For example, to specify that Mace4 and Prover9 have different time limits, one can write

if(Mace4).
  assign(max_seconds, 30).
end_if.

if(Prover9).
  assign(max_seconds, 3600).
end_if.

The conditional-inclusion construct cannot occur within a list of objects (formulas, weighting rules, etc.).

Next Section: Clauses & Formulas