{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T08:23:04Z","timestamp":1760170984952},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact same final state, confluence modulo equivalence only requires the final states to be equivalent with respect to an equivalence relation tailored for the given program. Secondly, we allow non-logical built-in predicates such as var\/1 and incomplete ones such as is\/2, that are ignored in previous work on confluence.<\/jats:p>\n          <jats:p>To this end, a new operational semantics for CHR is developed which includes such predicates. In addition, this semantics differs from earlier approaches by its simplicity without loss of generality, and it may also be recommended for future studies of CHR.<\/jats:p>\n          <jats:p>For the purely logical subset of CHR, proofs can be expressed in first-order logic, that we show is not sufficient in the present case. We have introduced a formal meta-language that allows reasoning about abstract states and derivations with meta-level restrictions that reflect the non-logical and incomplete predicates. This language represents subproofs as diagrams, which facilitates a systematic enumeration of proof cases, pointing forward to a mechanical support for such proofs.<\/jats:p>\n          <jats:p>The Project is supported by The DanishCouncil for IndependentResearch, Natural Sciences, Grant No. DFF4181-00442. The second author\u2019s contribution received funding from the European Union Seventh Framework Programme (FP7\/2007-2013) under Grant Agreement No. 318337, ENTRA\u2014Whole-Systems Energy Transparency.<\/jats:p>","DOI":"10.1007\/s00165-016-0396-9","type":"journal-article","created":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T05:11:52Z","timestamp":1479359512000},"page":"57-95","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["On proving confluence modulo equivalence for Constraint Handling Rules"],"prefix":"10.1145","volume":"29","author":[{"given":"Henning","family":"Christiansen","sequence":"first","affiliation":[{"name":"Research group PLIS: Programming, Logic and Intelligent Systems, Department of People and Technology, Roskilde University, Roskilde, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maja H.","family":"Kirkeby","sequence":"additional","affiliation":[{"name":"Research group PLIS: Programming, Logic and Intelligent Systems, Department of People and Technology, Roskilde University, Roskilde, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abdennadher S (1997) Operational semantics and confluence of constraint propagation rules. In: Smolka G (ed) CP Constraint Programming Lecture Notes in Computer Science vol 1330. Springer New York pp 252\u2013266","DOI":"10.1007\/BFb0017444"},{"key":"#cr-split#-e_1_2_1_2_2_2.1","doi-asserted-by":"crossref","unstructured":"Abdennadher S Fr\u00fchwirth TW (2003) Integration and optimization of rule-based constraint solvers. In: Bruynooghe M","DOI":"10.1007\/978-3-540-25938-1_17"},{"key":"#cr-split#-e_1_2_1_2_2_2.2","unstructured":"(ed) Logic Based Program Synthesis and Transformation 13th International Symposium LOPSTR 2003 Uppsala Sweden August 25-27 2003 Revised Selected Papers Lecture Notes in Computer Science vol 3018. Springer New York pp 198-213"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abdennadher S Fr\u00fchwirth TW Meuss H (1996) On confluence of Constraint Handling Rules. In: Freuder EC (ed) CP Lecture Notes in Computer Science vol 1118. Springer New York pp 1\u201315","DOI":"10.1007\/3-540-61551-2_62"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1009842826135"},{"key":"e_1_2_1_2_5_2","unstructured":"Aho AV Sethi R Ullman JD (1972) Code optimization and finite Church-Rosser systems. In: Rustin R (ed) Design and Optimization of Compilers. Prentice-Hall USA pp 89\u2013106"},{"key":"#cr-split#-e_1_2_1_2_6_2.1","doi-asserted-by":"crossref","unstructured":"Aiken A Widom J Hellerstein JM (1992) Behavior of database production rules: Termination confluence and observable determinism. In: Stonebraker M","DOI":"10.1145\/130283.130296"},{"key":"#cr-split#-e_1_2_1_2_6_2.2","unstructured":"(ed) Proceedings of the 1992 ACM SIGMOD International Conference on Management of Data San Diego California. ACM Press USA pp 59-68"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01190828"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/280474"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841000030X"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068405002395"},{"key":"e_1_2_1_2_11_2","unstructured":"Christiansen H Have CT Lassen OT Petit M (2010) The Viterbi algorithm expressed in Constraint Handling Rules. In: Van Weert P De Koninck L (eds) Proceedings of the 7th International Workshop on Constraint Handling Rules Report CW 588. Katholieke Universiteit Leuven Belgium pp 17\u201324"},{"key":"e_1_2_1_2_12_2","unstructured":"Christiansen H Kirkeby MH (2010) Confluence modulo equivalence in Constraint Handling Rules. In: Proietti M Seki H (eds) Logic-Based Program Synthesis and Transformation\u201424th International Symposium LOPSTR 2014 Canterbury UK September 9\u201311 2014. Revised Selected Papers Lecture Notes in Computer Science vol 8981. Springer New York pp 41\u201358"},{"key":"e_1_2_1_2_13_2","unstructured":"Drabent W (1997) A Floyd-Hoare method for Prolog. Tech. Rep. 2(13) Link\u00f6ping Electronic Articles in Computer and Information Science"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Duck GJ Stuckey PJ De la Banda MJG Holzbaur C (2004) The refined operational semantics of Constraint Handling Rules. In: Demoen B Lifschitz V (eds) Proc. Logic Programming 20th International Conference ICLP 2004 Lecture Notes in Computer Science vol 3132. Springer New York pp 90\u2013104","DOI":"10.1007\/978-3-540-27775-0_7"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Duck GJ Stuckey PJ Sulzmann M (2007) Observable confluence for Constraint Handling Rules. In: Dahl V Niemel\u00e4 I (eds) ICLP Lecture Notes in Computer Science vol 4670. Springer New York pp 224\u2013239","DOI":"10.1007\/978-3-540-74610-2_16"},{"key":"e_1_2_1_2_16_2","volume-title":"Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids","author":"Durbin R","year":"1999"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00328-9"},{"key":"e_1_2_1_2_18_2","unstructured":"Fr\u00fchwirth T Raiser F (eds) (2011) Constraint Handling Rules Compilation Execution and Analysis. Books on Demand GmbH. Norderstedt"},{"key":"e_1_2_1_2_19_2","unstructured":"Fr\u00fchwirth TW (1993) User-defined constraint handling. In: Warren DS (ed) Logic Programming Proceedings of the Tenth International Conference on Logic Programming. MIT Press Budapest Hungary pp 837\u2013838"},{"key":"#cr-split#-e_1_2_1_2_20_2.1","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth TW (1994) Constraint Handling Rules. In: Podelski A","DOI":"10.1007\/3-540-59155-9_6"},{"key":"#cr-split#-e_1_2_1_2_20_2.2","unstructured":"(ed) Constraint Programming: Basics and Trends Ch\u00e2tillon Spring School Ch\u00e2tillon-sur-Seine France May 16-20 1994 Selected Papers Lecture Notes in Computer Science vol 910. Springer New York pp 90-107"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609886"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068412000270"},{"key":"e_1_2_1_2_24_2","unstructured":"Hill P.; Gallagher J.: Meta-programming in logic programming. In: Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford Science Publications Oxford University Press Oxford pp 421\u2013497"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1080\/088395100117043"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Knuth D Bendix P (1970) Simple word problems in universal algebras. In: Leech J (ed) Computational Problems in Universal Algebras. Pergamon Press Oxford pp 263\u2013297","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"e_1_2_1_2_28_2","unstructured":"Langbein J Raiser F Fr\u00fchwirth TW (2010) A state equivalence and confluence checker for CHRs. In: Weert PV Koninck LD (eds) Proceedings of the 7th International Workshop on Constraint Handling Rules Report CW 588. Katholieke Universiteit Leuven Belgium pp 1\u20138"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003762"},{"key":"#cr-split#-e_1_2_1_2_32_2.1","unstructured":"Niehren J Smolka G (1994) A confluent relational calculus for higher-order programming with constraints. In: Jouannaud J"},{"key":"#cr-split#-e_1_2_1_2_32_2.2","unstructured":"(ed) Constraints in Computational Logics First International Conference CCL'94 Munich Germant September 7-9 1994 Lecture Notes in Computer Science vol 845. Springer New York pp 89-104"},{"key":"e_1_2_1_2_33_2","unstructured":"Raiser F Betz H Fr\u00fchwirth TW (2009) Equivalence of CHR states revisited. In: Raiser F Sneyers J (eds) Proc. 6th International Workshop on Constraint Handling Rules Report CW 555. Katholieke Universiteit Leuven Belgium pp 33\u201348"},{"key":"e_1_2_1_2_34_2","unstructured":"Raiser F Tacchella P (2007) On confluence of non-terminating CHR programs. In: Djelloul K Duck GJ Sulzmann M (eds) Constraint Handling Rules 4th Workshop CHR 2007. Porto Portugal pp 63\u201376"},{"key":"e_1_2_1_2_35_2","unstructured":"Personal communication with Tom Schrijvers (2016)"},{"key":"e_1_2_1_2_36_2","unstructured":"Schrijvers T Demoen B (2004) The K.U.Leuven CHR system: implementation and application. In: Fr\u00fchwirth T Meister M (eds) First Workshop on Constraint Handling Rules: Selected Contributions. Ulmer Informatik-Berichte Nr. 2004-01 pp 1\u20135"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Schrijvers T Fr\u00fchwirth TW (eds) (2008) Constraint Handling Rules Current Research Topics Lecture Notes in Computer Science vol 5388. Springer New York","DOI":"10.1007\/978-3-540-92243-8"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/321850.321862"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068409990123"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/62.2160"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1967.1054010"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0396-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0396-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0396-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0396-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:04:51Z","timestamp":1641485091000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0396-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1]]}},"alternative-id":["10.1007\/s00165-016-0396-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0396-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1]]}}}