Experience from real-life applications using constraint-based programming has shown that typically, one is confronted with a heterogeneous mix of different types of constraints. To be able to express constraints as they appear in the application and to write and combine constraint systems, a special purpose language for writing constraint systems called constraint handling rules (CHR) was developed. CHR have been used to encode a wide range of constraint handlers (solvers), including new domains such as terminological and temporal reasoning. Several CHR libraries exist in declarative languages such as Prolog and LISP, worldwide more than 20 projects use CHR. You can find more information about CHR in [Fruehwirth 98] or at http://www.informatik.uni-ulm.de/pm/mitarbeiter/fruehwirth/chr-intro.html
The high-level CHR 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 CHR in a straightforward way. Starting from this executable specification, the rules can be refined and adapted to the specifics of the application.
The CHR library includes a compiler, which translates CHR programs into Prolog programs on the fly, and a runtime system, which includes a stepper for debugging. Many constraint handlers are provided in the example directory of the library.
CHR are essentially a committed-choice language consisting of guarded
rules that rewrite constraints into simpler ones until they are solved.
CHR define both simplification of and propagation over
constraints. Simplification replaces constraints by
simpler constraints while preserving logical equivalence (e.g.
X>Y,Y>X <=> fail). Propagation adds new constraints that are
logically redundant but may cause further simplification (e.g.
X>Y,Y>Z ==> X>Z). Repeatedly applying CHR incrementally simplifies
and finally solves constraints (e.g. A>B,B>C,C>A)
leads to fail.
With multiple heads and propagation rules, CHR provide two features that are essential for non-trivial constraint handling. The declarative reading of CHR as formulas of first order logic allows one to reason about their correctness. On the other hand, regarding CHR as a rewrite system on logical formulas allows one to reason about their termination and confluence.
In case the implementation of CHR disagrees with your expectations
based on this chapter, drop a line to the current maintainer:
christian@ai.univie.ac.at (Christian Holzbaur).