constraints before the are kept, as a in a propagation rule; the remaining constraints are removed. Since simpagation rules subsume simplification and propagation, all CHR rules follow the format where each of is a conjunction of constraints: and contain CHR constraints, while the guards are built-in. Only one of needs to be non-empty. The host language must also define built-in constraints over terms. The guards in rules are built-in constraints, so they effectively execute host language code. The built-in constraint theory must include at least true (the constraint that always holds), fail (the constraint that never holds, and is used to signal failure) and equality of terms, i.e., unification. When the host language does not support these features, they must be implemented along with CHR. Execution of a CHR program starts with an initial constraint store. The program then proceeds by matching rules against the store and applying them, until either no more rules match (success) or the fail constraint is derived. In the former case, the constraint store can be read off by a host language program to look for facts of interest. Matching is defined as "one-way unification": it binds variables only on one side of the equation. Pattern matching can be easily implemented when as unification when the host language supports it. Example program The following CHR program, in Prolog syntax, contains four rules that implement a solver for a less-or-equal constraint. The rules are labeled for convenience (labels are optional in CHR). % X leq Y means variable X is less-or-equal to variable Y reflexivity @ X leq X <=> true. antisymmetry @ X leq Y, Y leq X <=> X = Y. transitivity @ X leq Y, Y leq Z ==> X leq Z. idempotence @ X leq Y \ X leq Y <=> true. The rules can be read in two ways. In the declarative reading, three of the rules specify the axioms of a partial ordering: Reflexivity: X ≤ X Antisymmetry: if X ≤ Y and Y ≤ X, then X = Y Transitivity: if X ≤ Y and Y ≤ Z, then X ≤ Z All three rules are implicitly universally quantified (upper-cased identifiers are variables in Prolog syntax). The idempotence rule is a tautology from the logical viewpoint, but has a purpose in the second reading of the program. The second way to read the above is as a computer program