{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,8]],"date-time":"2026-09-08T12:24:37Z","timestamp":1788870277015,"version":"build-2803163510"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Baden-W\u00fcrttemberg Federal State","award":["LGFG #0518"],"award-info":[{"award-number":["LGFG #0518"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,2]]},"abstract":"<jats:p>Constraint Handling Rules (CHR) is a declarative rule-based programming language that has cut out its niche over the course of the last 20 years. It generalizes concurrent constraint logic programming to multiple heads, thus closing the gap to multiset transformation systems. Its popular extension CHR with Disjunction (CHR\u2228) is a multiparadigm declarative programming language that allows embedding of Horn programs with SLD resolution.<\/jats:p>\n                  <jats:p>We analyze the assets and the limitations of the classical declarative semantics of CHR\u2228 and highlight its natural relationship with linear-logic. We furthermore develop two linear-logic semantics for CHR\u2228 that differ in the reasoning domain for which they are instrumental. We show their idempotence and their soundness and completeness with respect to the operational semantics. We show how to apply the linear-logic semantics to decide program properties and to reason about operational equivalence of CHR\u2228 programs.<\/jats:p>","DOI":"10.1145\/2422085.2422086","type":"journal-article","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T14:25:04Z","timestamp":1361543104000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Linear-Logic Based Analysis of Constraint Handling Rules with Disjunction"],"prefix":"10.1145","volume":"14","author":[{"given":"Hariolf","family":"Betz","sequence":"first","affiliation":[{"name":"University of Ulm"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thom","family":"Fr\u00fchwirth","sequence":"additional","affiliation":[{"name":"University of Ulm"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017444"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068405002371"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Abdennadher S.\n     and \n      Sch\u00fctz H\n  . \n  1998\n  . CHRv: \n  A\n   Flexible Query Language. In Proceedings of the 3rd International Conference on Flexible Query Answering Systems T. Andreasen H. Christiansen and H. L. Larsen Eds. Lecture Notes in Computer Science vol. \n  1495\n  . \n  Springer Berlin 1--14.   Abdennadher S. and Sch\u00fctz H. 1998. CHRv: A Flexible Query Language. In Proceedings of the 3rd International Conference on Flexible Query Answering Systems T. Andreasen H. Christiansen and H. L. Larsen Eds. Lecture Notes in Computer Science vol. 1495. Springer Berlin 1--14.","DOI":"10.1007\/BFb0055987"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Abdennadher S. Fruhwirth T. and \n      Meuss H\n  . \n  1996\n  . On confluence of constraint handling rules. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP\u201996) Lecture Notes in Computer Science vol. \n  1118\n  . \n  Springer-Verlag Berlin 1--15.  Abdennadher S. Fruhwirth T. and Meuss H. 1996. On confluence of constraint handling rules. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP\u201996) Lecture Notes in Computer Science vol. 1118. Springer-Verlag Berlin 1--15.","DOI":"10.1007\/3-540-61551-2_62"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1009842826135"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/97945.97953"},{"key":"e_1_2_2_9_1","volume-title":"Proceedings of the 4th Workshop on Constraint Handling Rules. 17--31","author":"Betz H.","year":"2007","unstructured":"Betz , H. 2007 . A linear logic semantics for constraint handling rules with disjunction . In Proceedings of the 4th Workshop on Constraint Handling Rules. 17--31 . Betz, H. 2007. A linear logic semantics for constraint handling rules with disjunction. In Proceedings of the 4th Workshop on Constraint Handling Rules. 17--31."},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Betz H.\n     and \n      Fr\u00fchwirth T. W\n  . \n  2005\n  . A linear-logic semantics for constraint handling rules. In Proceedings of the International Conference on Principles and Practice of Constraint Programming P. van Beek Ed. Lecture Notes in Computer Science vol. \n  3709\n  . \n  Springer Berlin 137--151.  Betz H. and Fr\u00fchwirth T. W. 2005. A linear-logic semantics for constraint handling rules. In Proceedings of the International Conference on Principles and Practice of Constraint Programming P. van Beek Ed. Lecture Notes in Computer Science vol. 3709. Springer Berlin 137--151.","DOI":"10.1007\/11564751_13"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841000030X"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Duck G. J. Stuckey P. J. de la Banda M. J. G. and \n      Holzbaur C\n  . \n  2004\n  . The refined operational semantics of constraint handling rules. In Proceedings of the International Conference on Logic Programming B. Demoen and V. Lifschitz Eds. Lecture Notes in Computer Science vol. \n  3132\n  . \n  Springer Berlin 90--104.  Duck G. J. Stuckey P. J. de la Banda M. J. G. and Holzbaur C. 2004. The refined operational semantics of constraint handling rules. In Proceedings of the International Conference on Logic Programming B. Demoen and V. Lifschitz Eds. Lecture Notes in Computer Science vol. 3132. Springer Berlin 90--104.","DOI":"10.1007\/978-3-540-27775-0_7"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the COMPULOG Workshop associated to the International Conference on Principles and Practice of Constraint Programming.","author":"Fages F.","unstructured":"Fages , F. , Ruet , P. , and Soliman , S . 1997. Linear concurrent constraint programming: Operational and phase semantics . In Proceedings of the COMPULOG Workshop associated to the International Conference on Principles and Practice of Constraint Programming. Fages, F., Ruet, P., and Soliman, S. 1997. Linear concurrent constraint programming: Operational and phase semantics. In Proceedings of the COMPULOG Workshop associated to the International Conference on Principles and Practice of Constraint Programming."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3002"},{"key":"e_1_2_2_16_1","volume-title":"Constraint Handling Rules","author":"Fr\u00fchwirth T.","unstructured":"Fr\u00fchwirth , T. 2009. Constraint Handling Rules . Cambridge University Press . Fr\u00fchwirth, T. 2009. Constraint Handling Rules. Cambridge University Press."},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth T. and Abdennadher S. 2003. Essentials of Constraint Programming. Springer-Verlag New York Inc. Secaucus NJ.   Fr\u00fchwirth T. and Abdennadher S. 2003. Essentials of Constraint Programming . Springer-Verlag New York Inc. Secaucus NJ.","DOI":"10.1007\/978-3-662-05138-2"},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming, A. Podelski Ed., Lecture Notes in Computer Science","volume":"910","author":"Fr\u00fchwirth T. W.","year":"1994","unstructured":"Fr\u00fchwirth , T. W. 1994 . Constraint handling rules . In Proceedings of the International Conference on Principles and Practice of Constraint Programming, A. Podelski Ed., Lecture Notes in Computer Science , vol. 910 . Springer, Berlin, 90--107. Fr\u00fchwirth, T. W. 1994. Constraint handling rules. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, A. Podelski Ed., Lecture Notes in Computer Science, vol. 910. Springer, Berlin, 90--107."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth T. W. Pierro A. D. and Wiklicky H. 2002. Probabilistic constraint handling rules. Electr. Notes Theor. Comput. Sci. 76.  Fr\u00fchwirth T. W. Pierro A. D. and Wiklicky H. 2002. Probabilistic constraint handling rules. Electr. Notes Theor. Comput. Sci. 76 .","DOI":"10.1016\/S1571-0661(04)80789-8"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the 5th Workshop on Constraint Handling Rules (CHR\u201908)","author":"Haemmerl\u00e9 R.","unstructured":"Haemmerl\u00e9 , R. and Betz , H . 2008. Verification of constraint handling rules using linear logic phase semantics . In Proceedings of the 5th Workshop on Constraint Handling Rules (CHR\u201908) . Haemmerl\u00e9, R. and Betz, H. 2008. Verification of constraint handling rules using linear logic phase semantics. In Proceedings of the 5th Workshop on Constraint Handling Rules (CHR\u201908)."},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the 5th International Conference on Algebraic Methodology and Software Technology (AMAST\u201996)","volume":"1101","author":"Harland J.","unstructured":"Harland , J. , Pym , D. J. , and Winikoff , M . 1996. Programming in Lygon: An overview . In Proceedings of the 5th International Conference on Algebraic Methodology and Software Technology (AMAST\u201996) , M. Wirsing and M. Nivat Eds., Lecture Notes in Computer Science , vol. 1101 . Springer, Berlin, 391--405. Harland, J., Pym, D. J., and Winikoff, M. 1996. Programming in Lygon: An overview. In Proceedings of the 5th International Conference on Algebraic Methodology and Software Technology (AMAST\u201996), M. Wirsing and M. Nivat Eds., Lecture Notes in Computer Science, vol. 1101. Springer, Berlin, 391--405."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069778"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Meister M. Djelloul K. and \n      Robin J\n  . \n  2007\n  . A unified semantics for constraint handling rules in transaction logic. In Proceedings of the International Conference on Logic Programming and Nonmonotonic Reasoning C. Baral G. Brewka and J. S. Schlipf Eds. Lecture Notes in Computer Science vol. \n  4483\n  . \n  Springer Berlin 201--213.   Meister M. Djelloul K. and Robin J. 2007. A unified semantics for constraint handling rules in transaction logic. In Proceedings of the International Conference on Logic Programming and Nonmonotonic Reasoning C. Baral G. Brewka and J. S. Schlipf Eds. Lecture Notes in Computer Science vol. 4483. Springer Berlin 201--213.","DOI":"10.1007\/978-3-540-72200-7_18"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the 3rd International Workshop on Extensions of Logic Programming (ELP\u201992)","volume":"660","author":"Miller D.","year":"1992","unstructured":"Miller , D. 1992 . The pi-calculus as a theory in linear logic: Preliminary results . In Proceedings of the 3rd International Workshop on Extensions of Logic Programming (ELP\u201992) , E. Lamma and P. Mello Eds., Lecture Notes in Computer Science , vol. 660 . Springer, Berlin, 242--264. Miller, D. 1992. The pi-calculus as a theory in linear logic: Preliminary results. In Proceedings of the 3rd International Workshop on Extensions of Logic Programming (ELP\u201992), E. Lamma and P. Mello Eds., Lecture Notes in Computer Science, vol. 660. Springer, Berlin, 242--264."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000633"},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the 6th International Workshop on Constraint Handling Rules (CHR), F. Raiser and J. Sneyers Eds., 34--48","author":"Raiser F.","unstructured":"Raiser , F. , Betz , H. , and Fr\u00fchwirth , T . 2009. Equivalence of CHR states revisited . In Proceedings of the 6th International Workshop on Constraint Handling Rules (CHR), F. Raiser and J. Sneyers Eds., 34--48 . Raiser, F., Betz, H., and Fr\u00fchwirth, T. 2009. Equivalence of CHR states revisited. In Proceedings of the 6th International Workshop on Constraint Handling Rules (CHR), F. Raiser and J. Sneyers Eds., 34--48."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_28"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462166.1462169"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92243-8_4"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/648039.744710"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422086","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2422085.2422086","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:18:35Z","timestamp":1750220315000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422086"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["10.1145\/2422085.2422086"],"URL":"https:\/\/doi.org\/10.1145\/2422085.2422086","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2]]},"assertion":[{"value":"2010-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}