### Abstract

The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

Language | English |
---|

Publisher | Computer Science, Roskilde University |
---|---|

Volume | 153 |

Number of pages | 20 |

State | Published - 3 Oct 2018 |

Series | Roskilde Universitet. Computer Science. Computer Science Research Report |
---|---|

Volume | 153 |

ISSN | 0109-9779 |

### Keywords

- confluence
- constraint handling rules
- observable confluence modulo equivalence; confluence modulo equivalence
- invariants
- equivalence

### Cite this

*Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]*. Computer Science, Roskilde University. Roskilde Universitet. Computer Science. Computer Science Research Report, Vol.. 153

}

*Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]*. Roskilde Universitet. Computer Science. Computer Science Research Report, vol. 153, vol. 153, Computer Science, Roskilde University.

**Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs].** / Christiansen, Henning; Kirkeby, Maja Hanne.

Research output: Book/Report › Report › Research

TY - RPRT

T1 - Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]

AU - Christiansen,Henning

AU - Kirkeby,Maja Hanne

PY - 2018/10/3

Y1 - 2018/10/3

N2 - Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

AB - Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

KW - confluence

KW - constraint handling rules

KW - observable confluence modulo equivalence; confluence modulo equivalence

KW - invariants

KW - equivalence

M3 - Report

VL - 153

BT - Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]

PB - Computer Science, Roskilde University

ER -