Prover9 Manual |  | Version 2009-02A

# Production Mode

Prover9's production mode allows for state-space searches. That is, it starts with

- one or more initial states,
- a set of production rules that lead from one state to the next, and
- one or more goal states.

The production mode is implemented by using Prover9's hyperreolution inference rule. Also, an enhanced form of rewriting (demodulation) is used, including

- evaluable functions and relations (implicit rules), such as integer arithmetic and Boolean operations;
- conditional rewrite rules which can apply to atomic formulas as well as to terms.

The rewriting is applied to the (instantiated) antecedents of the production rules as well as to the consequents.

The production mode is enabled by setting the following flag.

    set(production).
    clear(production).  % default clear

> The only direct effect of setting this flag is that it changes several options as follows.

>       set(production) -> set(raw).
>       set(produtcion) -> set(hyper_resolution).
>       set(produtcion) -> set(eval_rewrite).
>       set(produtcion) -> clear(back_subsume).

The `raw` option, which cancels many of the default Prover9 settings, is used because the production mode is quite different and more limited in nature from the ordinary mode of Prover9.

Here is a simple example which uses evaluable arithmetic operations (but no explicit rewrite rules).

    prover9 -f jugs.in > jugs.out

And here are two simple examples that use explicit rewrite rules.

    prover9 -f cabbages.in > cabbages.out

    prover9 -f queens3.in > queens3.out

Here is a more complex example.

    prover9 -f 2inverter.in > 2inverter.out

The following job shows examples of several list-processing functions.

    prover9 -f list.in > list.out

## Evaluable Operations

See the page Clauses and Formulas for the built-in parsing/printing declarations for these operations.

Functions on Integers
Operation | Comment
--- | ---
`+` | integer sum
`-` | integer negation (unary only) (used also for Boolean negation)
`/` | integer division
`mod` | modulus
`abs` | integer absolute value
`min` | integer minimum (binary)
`max` | integer maximum (binary)

Relations on Integers
Operation | Comment
--- | ---
`<` | less than
`<=` | less or equal
`>` | greater than
`>=` | greater or equal
`==` | equal (used also for non-integers)
`!==` | not equal (used also for non-integers)

Properties and Relations on Terms
Operation | Comment
--- | ---
`variable` | is the term a variable?
`constant` | is the term a constant (includes integers)?
`ground` | is the term variable-free?
`@<` | lexically less than
`@<=` | lexically less or equal
`@>` | lexically greater than
`@>=` | lexically greater or equal
`==` | identical (used also for integers)
`!==` | not identical (used also for integers)

Logic Operations
Operation | Comment
--- | ---
`&` | conjunction
`&&` | conjunction* (see below)
`|` | disjunction
`||` | disjunction* (see below)
`-` | negation (used also for integers)

Conditional Expressions
Operation | Comment
--- | ---
`if` | `if(condition, then_part, else_part)` (see Section Conditional Expressions)

*The double forms of the conjunction and disjunction operations (`&&` and `||`) are logically the same as the single forms (`&` and `|`); the double forms are used to prevent expansion of production rules. For example, if a production rule is written as

    P & (Q1 | Q2) -> R.

it will be expanded to the pair of clauses

    P & Q1 -> R.
    P & Q2 -> R.

by the clausification process. If Q1 and Q2 are evaluable, it is usually more efficient use the original form of the rule; using the double form of the disjunction operator prevents expansion:

    P & (Q1 || Q2) -> R.

The double forms never have to be used in rewrite rules.

## Enhanced Rewrite Rules for Production Mode

Ordinary Prover9 rewrite rules (demodulators) are always equations, which are used to rewrite terms. When in production mode, Prover9 can use enhanced rewrite rules, which can be conditional and which can rewrite atomic formulas as well as terms.

Equational rules rewrite terms, and equivalence rules rewrite atomic formulas. Either kind of rule can have conditions.

Many of the following examples use terms that are lists. Recall that lists are built from a binary constructor function `$cons` and well-formed lists are terminated with `$nil`. The term `[a:b]` abbreviates `$cons(a,b)`, and the term `[a,b,c]` abbreviates `$cons(a,$cons(b,$cons(c,$nil)))`.

### Equational Rules

Equational rules have one of the following forms.

    alpha = beta.    % unconditional
    condition -> alpha = beta.
    alpha = beta <- condition.

In each case, an instance of `alpha` is rewritten to the corresponding instance of `beta` if the corresponding instance of the `condition` (if present) rewrites to `$T` (true).

For example, the following three rewrite rules constitute a function that takes a term `z` and a list of terms, and returns the sublist of terms that are lexically greater than `z`.

    gt_list(z,[]) = [].
    x @>  z -> gt_list(z,[x:y]) = [x:gt_list(z,y)].
    x @<= z -> gt_list(z,[x:y]) = gt_list(z,y).

(These rewrite rules can be used to build a quicksort function, see list.in.)

### Equivalence Rules

Equivalence rules rewrite atomic formulas. The forms are similar to equational rules, but they have `<->` instead of `=` .

    alpha <-> beta.    % unconditional
    condition -> (alpha <-> beta).
    (alpha <-> beta) <- condition.

For example, the following three rules constitues a membership relation for lists.

    member(x,[]) <-> $F.
    x  == y  -> (member(x,[y:z]) <-> $T).
    x !== y  -> (member(x,[y:z]) <-> member(x,z)).

In equivalence rules the `alpha` expression must be an atomic formula, but the `beta` expression can be a non-atomic formula involving disjunction, conjunction, and negation. For example, the following pair of rules implements a subset relation on lists.

    subset([], x) <-> $T.
    subset([x:y], z) <-> member(x,z) & subset(y,z).

If the `beta` expression of an equivalence rule is `$T` or `$F`, the rule can be abbreviated in the obvious way. For example, the membership relation shown above can be abbreviated as follows.

    -member(x,[]).
    x  == y  -> member(x,[y:z]).
    x !== y  -> (member(x,[y:z]) <-> member(x,z)).

### Beware of the Distinction between Function and Relation Symbols (Terms and Atomic Formulas)

### Conditional Expressions (If-expressions)

Many rewrite rules can be written more conveniently with conditional expressions than with conditional rules. A conditional expression has the following form.

    if(condition, then_part, else_part)

When evaluating a conditional expression,

- if the condition evaluates to `$T`, the value of the expression is then_part;
- if the condition evaluates to `$F`, the value of the expression is else_part;
- if the condition evaluates to neither `$T` nor `$F`, the "`if`" expression is not evaluated (but the then_part and the else_part are evaluated); in this case, the result will contain an if-expression, indicating that something is probably wrong with it.

The condition of an if-expression must be an evaluable formula (Boolean-valued object). If the if-expression occurs in the context of a term, the then_part and the else_part must also be terms. If the if-expression occurs in the context of a formula, the then_part and the else_part must also be formulas.

Here are two examples of rules containing if-expressions. The membership relation has the if-expression in the context of a formula, and the intersection function has it in the context of a term.

    -member(x,[]).
    member(x,[y:z]) <-> if(x == y, $T, member(x,z)).

    intersect([], x) = [].
    intersect([x:y],z) = if(member(x,z),[x:intersect(y,z)],intersect(y,z)).

## Hyperresolution in Production Mode

The hyperresolution inference rule is used when Prover9 is in production mode. Recall that in hyperresolution all of the negative literals of the nucleus (antecedents of the production rule) must be operated on so that the result is a positive clause. In production mode, the negative literals (antecedents) are partitioned into resolvable literals and evaluable literals. Consider the production rule in one of the examples given above.

    J(x, y) & (x+y <= 4) -> J(0, y+x).           % empty the small jug into the big jug

The first antecedent is resolvable, because it is headed by the state predicate `J`, and the second is evalable, because it is headed by a built-in evaluable operation.

An antecedent can also be evaluable if it is headed by a defined evaluable operation; that is, there is an equivalence rewrite rule to evaluate it. Consider the production rule from 8-Queens example above (assume set(prolog_style_variables)).

    board(B) & pick(New_col) & ok(B, 1, New_col) -> board([New_col:B]).

The first two antecedents are resolvable: the first takes a state, and the second picks a column to try to fill in. The third antecedent is evaluable, because there are equivalence rule to evaluate it (in this case, it checks whether a state transition can take place).

    formulas(demodulators).

    ok([], X, Y) <-> $T.

    ok([H:T], Rows_back, New_col) <->
    	-(H == New_col) &
    	-(H + -Rows_back == New_col) &
    	-(H + Rows_back == New_col) &
    	ok(T, Rows_back+1, New_col).

    end_of_list.

## Justifications in Production Mode

When Prover9 is in production mode, clause justifications for hyperresolution are similar to those in ordinary mode, but justifications for rewriting (demodulation) is different, and there is a new kind of justfication for evaluation.

In ordinary mode, Prover9 shows the sequence of rewrite steps, with data on where the rewrite occurred and the direction of the rewrite. In production mode, Prover9 simply shows the set of rules that were applied. This difference is because in production mode, there can be extremely long sequences of rewrites.

When evaluation of a built-in evaluable operation occurs, Prover9 simply reports the number of evaluation steps. Consider a clause from the 8-Queens example above:

    board([6,3,1,4,8]).  [hyper(2,a,226,a,b,8,a),rewrite([13,12]),eval(40)].

The justification shows the two resolution steps, rewriting with two rules, and 40 evaluations with built-in operations.

Next Section: Advanced Features