for maintaining a constraint store, a collection of facts (constraints) about objects. The constraint store is not part of this program, but must be supplied separately. The rules express the following rules of computation: Reflexivity is a simplification rule: it expresses that, if a fact of the form X ≤ X is found in the store, it may be removed. Antisymmetry is also a simplification rule, but with two heads. If two facts of the form X ≤ Y and Y ≤ X can be found in the store (with matching X and Y), then they can be replaced with the single fact X = Y. Such an equality constraint is considered built in, and implemented as a unification that is typically handled by the underlying Prolog system. Transitivity is a propagation rule. Unlike simplification, it does not remove anything from the constraint store; instead, when facts of the form X ≤ Y and Y ≤ Z (with the same value for Y) are in the store, a third fact X ≤ Z may be added. Idempotence, finally, is a simpagation rule, a combined simplification and propagation. When it finds duplicate facts, it removes them from the store. Duplicates may occur because constraint stores are multi-sets of facts. Given the query A leq B, B leq C, C leq A the following transformations may occur: The transitivity rule adds A leq C. Then, by applying the antisymmetry rule, A leq C and C leq A are removed and replaced by A = C. Now the antisymmetry rule becomes applicable on the first two constraints of the original query. Now all CHR constraints are eliminated, so no further rules can be applied, and the answer A = B, A = C is returned: CHR has correctly inferred that all three variables must refer to the same object. Execution of CHR programs To decide which rule should "fire" on a given constraint store, a CHR implementation must use some pattern matching algorithm. Candidate algorithms include RETE and TREAT, but most implementation use a lazy algorithm called LEAPS. The original specification of CHR's semantics was entirely non-deterministic, but the so-called "refined operation semantics" of Duck et al. removed much of the non-determinism so that application writers can rely on the order of execution for performance and correctness of their programs. Most applications of CHRs require that the rewriting process be confluent; otherwise the