Confluence of CHR Revisited: Invariants and Modulo Equivalence

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

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 HThe invariant is formalizedandling 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.
OriginalsprogEngelsk
TitelLogic-Based Program Synthesis and Transformation : 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers
RedaktørerFred Mesnard, Peter J. Stuckey
Vol/bind11408
Udgivelses stedCham
ForlagSpringer
Publikationsdato2019
Sider94-111
ISBN (Trykt)978-3-030-13837-0
ISBN (Elektronisk)978-3-030-13838-7
DOI
StatusUdgivet - 2019
BegivenhedLOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation - Göthe-University Frankfurt am Main, Frankfurt am Main, Tyskland
Varighed: 4 sep. 20186 sep. 2018
Konferencens nummer: 28
http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html

Konference

KonferenceLOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation
Nummer28
LokationGöthe-University Frankfurt am Main
LandTyskland
ByFrankfurt am Main
Periode04/09/201806/09/2018
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind11408
ISSN0302-9743
NavnTheoretical Computer Science and General Issues
Vol/bind11408

Emneord

  • Constraint Handling Rules
  • Confluence
  • Confluence modulo equivalence
  • Invariants
  • Observable confluence

Citer dette