Content deleted Content added
→Constraint handling rules: slight rewriting of how to specify a satisfiability method |
→Bottom-up evaluation: termination using entailment |
||
Line 131:
In the above example, the only used facts were ground literals. In general, every clause that only contains constraints in the body is considered a fact. For example, a clause <code>A(X):-X>0,X<10</code> is considered a fact as well. For this extended definition of facts, some facts may be equivalent while not syntactically equal. For example, <code>A(q)</code> is equivalent to <code>A(X):-X=q</code> and both are equivalent to <code>A(X):-X=Y, Y=a</code>. To solve this problem, facts are translated into a normal form in which the head contains a tuple of all-different variables; two facts are then equivalent if their bodies are equivalent on the variables of the head, that is, their sets of solutions are the same when restricted to these variables.
As described, the bottom-up approach has the advantage of not considering consequences that have already been derived. However, it still may derive consequences that are entailed by those already derived while not being equal to any of them. As an example, the bottom up evaluation of the following program is infinite:
A(0).
A(X):-X>0.
A(X):-X=Y+1, A(X).
The bottom-up evaluation algorithm first derives that <code>A(X)</code> is true for <code>X=0</code> and <code>X>0</code>. In the second step, the first fact with the third clause allows for the derivation of <code>A(1)</code>. In the third step, <code>A(2)</code> is derived, etc. However, these facts are already entailed by the fact that <code>A(X)</code> is true for any nonnegative <code>X</code>. This drawback can be overcome by checking for entailment facts that are to be added to the current set of consequences. If the new consequence is already entailed by the set, it is not added to it. Since facts are stored as clauses, possibly with "local variables", entailment is restricted over the variables of their heads.
==History==
| |||