11.1 Unification as Constraint Solving

Unification is the process of solving constraints. The Oz constraint store contains only constraints in solved form. Whenever a constraint is told to the constraint store, unification becomes active and computes a new normal form. This new normal form is logically equivalent to the conjunction of the previous normal form and the newly added constraint.

Of course it can happen that a constraint told is inconsistent with the actual constraint store. In this case, unification fails and no constraint is added to the constraint store. Failure can be considered as logical information or as programming error. This will be explained later.