| Prover9 Manual |
| Version 2009-11A |
The production mode is implemented by using Prover9's hyperreolution inference rule. Also, an enhanced form of rewriting (demodulation) is used, including
The production mode is enabled by setting the following flag.
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).
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).
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.
| 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) |
| 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) |
| 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) |
| Operation | Comment |
|---|---|
| & | conjunction |
| && | conjunction* (see below) |
| | | disjunction |
| || | disjunction* (see below) |
| - | negation (used also for integers) |
| 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.
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))).
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.)
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)).
if(condition, then_part, else_part)When evaluating a conditional expression,
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)).
J(x, y) & (x+y <= 4) -> J(0, y+x). % empty the small jug into the big jugThe 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.
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.