|
A(X,Y):-X>0, B(X,Y).
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>. Contrarily to regular logic programming, the constraint <code>X>0</code> in the body of the last clause isthis also required to be satisfied by the solution. On the other hand, the value of <code>X</code> is not determined at this point. Asrequires a result, whether this constraint willto be satisfied cannot yet be determined. Rather than proceeding in the evaluation of: <code>B(X,1)</code> and then checking whether the resulting value of <code>X0</code> is positive afterwards, the interpreter stores the constraint <code>X>0</code> and then proceed in the evaluationbody of <code>B(X,1)</code>; this way, the interpreterlast can check whether the constraint <code>X>0</code> is unsatisfiable during the evaluation of <code>B(X,1)</code> rather than afterwardsclause.
In general, the evaluation ofWhether a constraint logicis programsatisfied proceedscannot likealways forbe adetermined regularwhen logicthe program,constraint but constraintis encountered. duringIn evaluationthis arecase, placed in a set called constraint store. As anfor example, the evaluationvalue of the goal <code>A(X,1)</code> proceedsis bynot evaluatingdetermined when the bodylast ofclause theis firstevaluated. clauseAs witha <code>Y=1</code>;result, thisthe evaluation addsconstraint <code>X>0</code> tois thenot constraintsatisfied storenor andviolated requiresat this point. Rather than proceeding in the goalevaluation of <code>B(X,1)</code> toand bethen proved.checking Whilewhether tryingthe toresulting provevalue thisof goal,<code>X</code> theis secondpositive clauseafterwards, isthe applicable,interpreter butstores itsthe evaluation addsconstraint <code>X<>0</code> toand thethen constraintproceed store; this addition makesin the constraintevaluation storeof unsatisfiable<code>B(X,1)</code>; andthis the interpreter backtracksway, removing the lastinterpreter additioncan fromdetect the constraint store. The evaluationviolation of the third clause addsconstraint <code>X=1>0</code> andduring the evaluation of <code>Y>0B(X,1)</code>, toand thebacktrack constraintimmediately store.if Since the constraint storethis is satisfiablethe andcase, norather otherthan literalwaiting is left to prove,for the interpreterevaluation stops with the solutionof <code>B(X=1, Y=1)</code> to conclude.
In general, the evaluation of a constraint logic program proceeds like for a regular logic program, but constraint encountered during evaluation are placed in a set called constraint store. As an example, the evaluation of the goal <code>A(X,1)</code> proceeds by evaluating the body of the first clause with <code>Y=1</code>; this evaluation adds <code>X>0</code> to the constraint store and requires the goal <code>B(X,1)</code> to be proved. While trying to prove this goal, the second clause is applicable, but its evaluation adds <code>X<0</code> to the constraint store. This addition makes the constraint store unsatisfiable, and the interpreter backtracks, removing the last addition from the constraint store. The evaluation of the third clause adds <code>X=1</code> and <code>Y>0</code> to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution <code>X=1, Y=1</code>.
==Semantics==
|
