the evaluation of B(X,1) and then checking whether the resulting value of X is positive afterwards, the interpreter stores the constraint X>0 and then proceeds in the evaluation of B(X,1); this way, the interpreter can detect violation of the constraint X>0 during the evaluation of B(X,1), and backtrack immediately if this is the case, rather than waiting for the evaluation of B(X,1) to conclude. In general, the evaluation of a constraint logic program proceeds as does a regular logic program. However, constraints encountered during evaluation are placed in a set called a constraint store. As an example, the evaluation of the goal A(X,1) proceeds by evaluating the body of the first clause with Y=1; this evaluation adds X>0 to the constraint store and requires the goal B(X,1) to be proven. While trying to prove this goal, the first clause is applied but its evaluation adds X<0 to the constraint store. This addition makes the constraint store unsatisfiable. The interpreter then backtracks, removing the last addition from the constraint store. The evaluation of the second clause adds X=1 and Y>0 to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution X=1, Y=1. Semantics The semantics of constraint logic programs can be defined in terms of a virtual interpreter that maintains a pair during execution. The first element of this pair is called current goal; the second element is called constraint store. The current goal contains the literals the interpreter is trying to prove and may also contain some constraints it is trying to satisfy; the constraint store contains all constraints the interpreter has assumed satisfiable so far. Initially, the current goal is the goal and the constraint store is empty. The interpreter proceeds by removing the first element from the current goal and analyzing it. The details of this analysis are explained below, but in the end this analysis may produce a successful termination or a failure. This analysis may involve recursive calls and addition of new literals to the current goal and new constraint to the constraint store. The interpreter backtracks if a failure is generated. A successful termination is generated when the current goal is empty and the constraint store is satisfiable. The details of the analysis of a literal removed from the goal is as follows. After having removed this literal from the front