Skip to main content
Erschienen in:
Buchtitelbild

1996 | ReviewPaper | Buchkapitel

On confluence of Constraint Handling Rules

verfasst von : Slim Abdennadher, Thom Frühwirth, Holger Meuss

Erschienen in: Principles and Practice of Constraint Programming — CP96

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

We introduce the notion of confluence for Constraint Handling Rules (CHR), a powerful language for writing constraint solvers. With CHR one simplifies and solves constraints by applying rules. Confluence guarantees that a CHR program will always compute the same result for a given set of constraints independent of which rules are applied. We give a decidable, sufficient and necessary syntactic condition for confluence.Confluence turns out to be an essential syntactical property of CHR programs for two reasons. First, confluence implies correctness (as will be shown in this paper). In a correct CHR program, application of CHR rules preserves logical equivalence of the simplified constraints. Secondly, even when the program is already correct, confluence is highly desirable. Otherwise, given some constraints, one computation may detect their inconsistency while another one may just simplify them into a still complex constraint.As a side-effect, the paper also gives soundness and completeness results for CHR programs. Due to their special nature, and in particular correctness, these theorems are stronger than what holds for the related families of (concurrent) constraint programming languages.

Metadaten
Titel
On confluence of Constraint Handling Rules
verfasst von
Slim Abdennadher
Thom Frühwirth
Holger Meuss
Copyright-Jahr
1996
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-61551-2_62