Prover9 Manual Version 2009-02A

Production Mode

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

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

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, 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