Observable confluence for constraint handling rules

Gregory J. Duck, Peter J. Stuckey, Martin Sulzmann

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

24 Citations (Scopus)


Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating CHR programs there is a decidable test for confluence. But many CHR programs that are in practice confluent fail this confluence test. The problem is that the states that illustrate non-confluence are not observable from the initial goals of interest. In this paper we introduce the notion of observable confluence, a more general notion of confluence which takes into account whether states are observable. We devise a test for observable confluence which allows us to verify observable confluence for a range of CHR programs dealing with agents, type systems, and the union-find algorithm.

Original languageEnglish
Title of host publicationLogic Programming - 23rd International Conference, ICLP 2007, Proceedings
Number of pages16
Publication statusPublished - 1 Dec 2007
Externally publishedYes
EventInternational Conference on Logic Programming 2007 - Porto, Portugal
Duration: 8 Sep 200713 Sep 2007
Conference number: 23rd
https://link.springer.com/book/10.1007/978-3-540-74610-2 (Proceedings)

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4670 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Logic Programming 2007
Abbreviated titleICLP 2007
Internet address

Cite this