Automatic Support for Proving Confluence Modulo Equivalence for Constraint Handling Rules

Project: Research

Project Details


Constraint Handling Rules, CHR, is a programming language consisting of rewrite rules over sets of logical atoms. CHR has become an important language for various forms of logic reasoning and application. A desired property of a CHR program is confluence, i.e., the final state, i.e., the result of running the program, is independent of the order in which the rules are applied. A confluent program may be optimized by a control of the rule order or parallel execution, and a proof of confluence is often involved in the proof of program correctness.
This project aims at extending existing results on proving confluence for CHR programs to confluence modulo an equivalence relation (CME). Given an equivalence relation ≈, a program is CME whenever alternative end states are equivalent modulo ≈. CME is highly relevant for CHR as it extends the notion of confluence to a much larger class of programs, including dynamic programming algorithms with pruning (such as Viterbi and Dijkstra's shortest path) and programs with redundant data structures (e.g., representing sets as lists or trees as in Union-Find).
Effective start/end date01/11/201531/12/2018


  • Det Frie Forskningsråd | Natur og Univers: €311,134.00

Research Output

  • 1 Journal article

On proving confluence modulo equivalence for Constraint Handling Rules

Christiansen, H. & Kirkeby, M. H., 2017, In : Formal Aspects of Computing. 29, 1, p. 57-95

Research output: Contribution to journalJournal articleResearchpeer-review

Open Access


  • 2 Participation in workshop, seminar, course
  • 1 Organisation and participation in conference

The 26th International Workshop on Functional and Logic Programming

Henning Christiansen (Speaker), & Maja Hanne Kirkeby (Speaker)

6 Sep 2018

Activity: Participating in or organising an eventParticipation in workshop, seminar, course

7th International Workshop on Confluence

Henning Christiansen (Speaker)

7 Jul 2018

Activity: Participating in or organising an eventParticipation in workshop, seminar, course

LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation

Henning Christiansen (Speaker), & Maja Hanne Kirkeby (Speaker)

4 Sep 20186 Sep 2018

Activity: Participating in or organising an eventOrganisation and participation in conference