Constraint handling rules (CHRs, CHR home page http://www.cs.kuleuven.ac.be/~dtai/projects/CHR/) [6] are a high-level language extension to write user-defined constraints. CHRs consists of guarded rules with multiple heads.
The high-level CHRs are an excellent tool for rapid prototyping and implementation of constraint handlers. The usual abstract formalism to describe a constraint system, i.e. inference rules, rewrite rules, sequents, formulas expressing axioms and theorems, can be written as CHRs in a straightforward way. Starting from this executable specification, the rules can be refined and adapted to the specifics of the application.
CHRs define simplification of, and propagation over, user-defined constraints. Simplification replaces constraints by simpler constraints while preserving logical equivalence (e.g. X>Y,Y>X <=> fail). Propagation adds new constraints which are logically redundant but may cause further simplification (e.g. X>Y,Y>Z ==> X>Z). Repeatedly applying CHRs incrementally simplifies and finally solves user-defined constraints (e.g. A>B,B>C,C>A leads to fail).
With multiple heads and propagation rules, CHRs provide two features which are essential for non-trivial constraint handling. The declarative reading of CHRs as formulas of first order logic allows one to reason about their correctness. On the other hand, regarding CHRs as a rewrite system on logical formulas allows one to reason about their termination and confluence.
In the next section it is explained how to use CHRs. Then, example constraint handlers and the colour graphic demo are listed. The next section introduces the basics of the CHR language and how it works. The next section describes more of the CHR language, the section after the built-in labeling feature. Then there is a section on how to write good CHR programs. Next the debuggers for CHRs are introduced.