Prover9 Manual |  | Version 2009-02A

# 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