Content deleted Content added
spelling |
m Task 70: Update syntaxhighlight tags - remove use of deprecated <source> tags |
||
Line 8:
Formally, constraint logic programs are like regular logic programs, but the body of clauses can contain constraints, in addition to the regular logic programming literals. As an example, <code>X>0</code> is a constraint, and is included in the last clause of the following constraint logic program.
<
B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).
</syntaxhighlight>
Like in regular logic programming, evaluating a goal such as <code>A(X,1)</code> requires evaluating the body of the last clause with <code>Y=1</code>. Like in regular logic programming, this in turn requires proving the goal <code>B(X,1)</code>. Contrary to regular logic programming, this also requires a constraint to be satisfied: <code>X>0</code>, the constraint in the body of the last clause (in regular logic programming, X>0 cannot be proved unless X is bound to a fully [[ground term]] and execution of the program will fail if that is not the case).
Line 163:
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(Y).
</syntaxhighlight>
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.
| |||