@book{3ebc1c4a5d4348beb79a5d6836e8f255,
title = "Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]",
abstract = "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.",
keywords = "confluence, constraint handling rules, observable confluence modulo equivalence; confluence modulo equivalence, invariants, equivalence, confluence, constraint handling rules, observable confluence modulo equivalence; confluence modulo equivalence, invariants, equivalence",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
year = "2018",
month = oct,
day = "3",
language = "English",
isbn = "0109-9779",
volume = "153",
series = "Roskilde Universitet. Computer Science. Computer Science Research Report",
publisher = "Roskilde Universitet",
}