Abstract: 

Constraint Handling Rules (CHR) is a high-level language for writing
constraint solvers either from scratch or by modifying existing
solvers.

In this work we refine the operational semantics of Constraint
Handling Rules. The new operational semantics is more faithful to the
actual implementations of CHR.  Then we give soundness and
completeness results for CHR programs.

Typically, more than one CHR rule is applicable to a conjunction of
constraints.  It is obviously desirable that the result of a
computation in a solver will always be the same, semantically and
syntactically, no matter which of the applicable CHR rules is
applied.  This essential syntactical property of any constraint solver
will be called confluence and will be investigated in this work.
Confluence ensures that the solver will always compute the same result
for a given set of constraints independent of which rules are applied.
It also means that it does not matter for the result in which order
the constraints arrive at the constraint solver.  We will introduce a
decidable, sufficient and necessary syntactic condition for confluence
of terminating CHR programs.  This condition adopts the notion of
critical pairs as known from term rewriting systems. A straightforward
translation of the results in this field was not possible, because the
CHR formalism gives rise to phenomena not appearing in term
rewriting systems. Moreover, as will be shown in this work,
confluence of a program implies consistency of its logical meaning
(under a mild restriction).

After introducing the notion of confluence for CHR, we investigate
completion methods to make a non-confluent CHR program confluent (if
possible).

Finally, we present practical applications of constraint programming
implemented with CHR.  The focus of this work is to show that
simplicity, flexibility, efficiency and rapid prototyping are 
advantages of CHR.