interpreter adds t1=t2 to the goal whenever a literal P(...t1...) is replaced with the body of a clause fresh variant whose head is P(...t2...). Tree terms Constraint logic programming with tree terms emulates regular logic programming by storing substitutions as constraints in the constraint store. Terms are variables, constants, and function symbols applied to other terms. The only constraints considered are equalities and disequalities between terms. Equality is particularly important, as constraints like t1=t2 are often generated by the interpreter. Equality constraints on terms can be simplified, that is solved, via unification: A constraint t1=t2 can be simplified if both terms are function symbols applied to other terms. If the two function symbols are the same and the number of subterms is also the same, this constraint can be replaced with the pairwise equality of subterms. If the terms are composed of different function symbols or the same functor but on different number of terms, the constraint is unsatisfiable. If one of the two terms is a variable, the only allowed value the variable can take is the other term. As a result, the other term can replace the variable in the current goal and constraint store, thus practically removing the variable from consideration. In the particular case of equality of a variable with itself, the constraint can be removed as always satisfied. In this form of constraint satisfaction, variable values are terms. Reals Constraint logic programming with real numbers uses real expressions as terms. When no function symbols are used, terms are expressions over reals, possibly including variables. In this case, each variable can only take a real number as a value. To be precise, terms are expressions over variables and real constants. Equality between terms is a kind of constraint that is always present, as the interpreter generates equality of terms during execution. As an example, if the first literal of the current goal is A(X+1) and the interpreter has chosen a clause that is A(Y-1):-Y=1 after rewriting is variables, the constraints added to the current goal are X+1=Y-1 and . The rules of simplification used for function symbols are obviously not used: X+1=Y-1 is not unsatisfiable just because the first expression is built using + and the second using -. Reals and function symbols can be combined, leading to terms that are expressions over reals and function symbols applied to other terms. Formally, variables and real constants