{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:53Z","timestamp":1750309133427,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,11,18]],"date-time":"2023-11-18T00:00:00Z","timestamp":1700265600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,1,31]]},"abstract":"<jats:p>\n            In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints (\u2112\n            <jats:sub>|\u22c5|<\/jats:sub>\n            ) to a decision procedure for \u2112\n            <jats:sub>|\u22c5|<\/jats:sub>\n            extended with set terms denoting finite integer intervals (\u2112\n            <jats:sub>[]<\/jats:sub>\n            ). In \u2112\n            <jats:sub>[]<\/jats:sub>\n            interval limits can be integer linear terms including\n            <jats:italic>unbounded variables<\/jats:italic>\n            . These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for \u2112\n            <jats:sub>[]<\/jats:sub>\n            it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the {\n            <jats:italic>log<\/jats:italic>\n            } (\u2018setlog\u2019) tool. The paper includes a case study based on the elevator algorithm showing that {\n            <jats:italic>log<\/jats:italic>\n            } can automatically discharge all its invariance lemmas, some of which involve intervals.\n          <\/jats:p>","DOI":"10.1145\/3625230","type":"journal-article","created":{"date-parts":[[2023,9,23]],"date-time":"2023-09-23T04:34:54Z","timestamp":1695443694000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[{"name":"Universidad Nacional de Rosario and CIFASIS, Argentina"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6970-8790","authenticated-orcid":false,"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Parma, Italy"}]}],"member":"320","published-online":{"date-parts":[[2023,11,18]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_3_3_3_2","doi-asserted-by":"crossref","unstructured":"M.\n      Leuschel\n     and \n      M.\n      Butler\n  . \n  2003\n  . ProB: \n  A\n   model checker for B. In FME Vol. \n  2805\n   of \n  Lecture Notes in Computer Science\n  . A. Keijiro S. Gnesi D. Mandrioli (Eds.) Springer-Verlag 855\u2013874.  M. Leuschel and M. Butler. 2003. ProB: A model checker for B. In FME Vol. 2805 of Lecture Notes in Computer Science . A. Keijiro S. Gnesi D. Mandrioli (Eds.) Springer-Verlag 855\u2013874.","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_3_3_4_2","unstructured":"Clearsy Atelier B home page http:\/\/www.atelierb.eu\/  Clearsy Atelier B home page http:\/\/www.atelierb.eu\/"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45988-X_9"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(4:12)2018"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068421000521"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.035"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/365151.365169"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09520-4"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09589-w"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00147-6"},{"key":"e_1_3_3_15_2","volume-title":"http:\/\/www.clpset.unipr.it\/setlog.Home.html, last access 2022","author":"Rossi G.","year":"2008","unstructured":"G. Rossi . 2008. \\(\\lbrace log\\rbrace\\) , http:\/\/www.clpset.unipr.it\/setlog.Home.html, last access 2022 ( 2008 ). G. Rossi. 2008. \\(\\lbrace log\\rbrace\\) , http:\/\/www.clpset.unipr.it\/setlog.Home.html, last access 2022 (2008)."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09577-6"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09602-2"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002730"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39197-3_13"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.024"},{"key":"e_1_3_3_22_2","unstructured":"M. Cristi\u00e1 and G. Rossi. 2019. Rewrite rules for a solver for sets binary relations and partial functions. Tech. rep.https:\/\/www.clpset.unipr.it\/SETLOG\/calculus.pdf  M. Cristi\u00e1 and G. Rossi. 2019. Rewrite rules for a solver for sets binary relations and partial functions. Tech. rep. https:\/\/www.clpset.unipr.it\/SETLOG\/calculus.pdf"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02149-8_20"},{"key":"e_1_3_3_24_2","doi-asserted-by":"crossref","unstructured":"M.\n      Cristi\u00e1 G.\n      Rossi and \n      C. S.\n      Frydman\n  . \n  2013\n  .  \\(\\lbrace log\\rbrace\\)  as a test case generator for the Test Template Framework. In SEFM R. M. Hierons M. G. Merayo M. Bravetti (Eds.) Vol. \n  8137\n   of \n  Lecture Notes in Computer Science Springer 229\u2013243.  M. Cristi\u00e1 G. Rossi and C. S. Frydman. 2013.  \\(\\lbrace log\\rbrace\\)  as a test case generator for the Test Template Framework. In SEFM R. M. Hierons M. G. Merayo M. Bravetti (Eds.) Vol. 8137 of Lecture Notes in Computer Science Springer 229\u2013243.","DOI":"10.1007\/978-3-642-40561-7_16"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"e_1_3_3_26_2","doi-asserted-by":"crossref","unstructured":"D.\n      Mentr\u00e9 C.\n      March\u00e9 J.-C.\n      Filli\u00e2tre and \n      M.\n      Asuka\n  . \n  2012\n  . Discharging proof obligations from Atelier B using multiple automated provers. In ABZ J. Derrick J. A. Fitzgerald S. Gnesi S. Khurshid M. Leuschel S. Reeves E. Riccobene (Eds.) Vol. \n  7316\n   of \n  Lecture Notes in Computer Science Springer 238\u2013251.  D. Mentr\u00e9 C. March\u00e9 J.-C. Filli\u00e2tre and M. Asuka. 2012. Discharging proof obligations from Atelier B using multiple automated provers. In ABZ J. Derrick J. A. Fitzgerald S. Gnesi S. Khurshid M. Leuschel S. Reeves E. Riccobene (Eds.) Vol. 7316 of Lecture Notes in Computer Science Springer 238\u2013251.","DOI":"10.1007\/978-3-642-30885-7_17"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022323717928"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-007-9017-9"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104498"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876639"},{"key":"e_1_3_3_31_2","volume-title":"Proceedings of the 10th International Joint Conference on Artificial Intelligence","author":"Ladkin P. B.","year":"1987","unstructured":"P. B. Ladkin . 1987 . The completeness of a natural system for reasoning with time intervals . In Proceedings of the 10th International Joint Conference on Artificial Intelligence . Milan, Italy , August 23-28, 1987, Morgan Kaufmann, J. P. McDermott (Ed.), 462\u2013465. DOI:http:\/\/ijcai.org\/Proceedings\/87-1\/Papers\/091.pdf P. B. Ladkin. 1987. The completeness of a natural system for reasoning with time intervals. In Proceedings of the 10th International Joint Conference on Artificial Intelligence. Milan, Italy, August 23-28, 1987, Morgan Kaufmann, J. P. McDermott (Ed.), 462\u2013465. DOI:http:\/\/ijcai.org\/Proceedings\/87-1\/Papers\/091.pdf"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-46714-2_6"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625230","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3625230","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:03Z","timestamp":1750287003000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625230"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,18]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1,31]]}},"alternative-id":["10.1145\/3625230"],"URL":"https:\/\/doi.org\/10.1145\/3625230","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,11,18]]},"assertion":[{"value":"2022-11-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-08-29","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}