{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T02:06:21Z","timestamp":1784167581299,"version":"3.55.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,1,16]],"date-time":"2024-01-16T00:00:00Z","timestamp":1705363200000},"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            We give a positive solution to the decidability problem for the fragment of set theory, dubbed\n            <jats:sans-serif>BST<\/jats:sans-serif>\n            \u2297, consisting of quantifier-free formulae involving the Boolean set operators of union, intersection, and set difference, along with the unordered Cartesian product operator \u2297 (where\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(s \\otimes t := \\big \\lbrace \\lbrace u,v\\rbrace \\,\\texttt {|}\\:u \\in s \\wedge v \\in t \\big \\rbrace\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            ), and the equality predicate, but no membership. Specifically, we provide nondeterministic exponential decision procedures for both the ordinary and the finite satisfiability problems for\n            <jats:sans-serif>BST<\/jats:sans-serif>\n            \u2297. We expect that these decision procedures can be adapted for the standard Cartesian product and, with added technicalities, to the cases involving membership, providing a solution to a longstanding problem in computable set theory.\n          <\/jats:p>","DOI":"10.1145\/3626823","type":"journal-article","created":{"date-parts":[[2023,10,6]],"date-time":"2023-10-06T15:45:02Z","timestamp":1696607102000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Decidability of the Satisfiability Problem for Boolean Set Theory with the Unordered Cartesian Product Operator"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1306-1166","authenticated-orcid":false,"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[{"name":"Dipartimento di Matematica e Informatica,Universit\u00e0 di Catania, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1477-2514","authenticated-orcid":false,"given":"Pietro","family":"Ursino","sequence":"additional","affiliation":[{"name":"Dipartimento di Matematica e Informatica,Universit\u00e0 di Catania, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,16]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/120986.120988"},{"key":"e_1_3_2_3_2","volume-title":"Bull. EATCS 39","author":"Cantone D.","year":"1989","unstructured":"D. Cantone and V. Cutello . 1989. Decision procedures for elementary sublanguages of set theory. XVI. Multilevel syllogistic extended by singleton, rank comparison and unary intersection . Bull. EATCS 39 , ( 1989 ), 139\u2013148. D. Cantone and V. Cutello. 1989. Decision procedures for elementary sublanguages of set theory. XVI. Multilevel syllogistic extended by singleton, rank comparison and unary intersection. Bull. EATCS 39, (1989), 139\u2013148."},{"key":"e_1_3_2_4_2","volume-title":"3rd Workshop on Computer Science Logic. 65\u201375","author":"Cantone D.","unstructured":"D. Cantone , V. Cutello , and A. Policriti . 1989. Set-theoretic reductions of Hilbert\u2019s tenth problem . In 3rd Workshop on Computer Science Logic. 65\u201375 . D. Cantone, V. Cutello, and A. Policriti. 1989. Set-theoretic reductions of Hilbert\u2019s tenth problem. In 3rd Workshop on Computer Science Logic. 65\u201375."},{"key":"e_1_3_2_5_2","volume-title":"3rd Workshop on Computer Science Logic (CSL\u201990)","author":"Cantone D.","unstructured":"D. Cantone , V. Cutello , and J. T. Schwartz . 1990. Decision problems for Tarski\u2019s and Presburger\u2019s arithmetics extended with sets . In 3rd Workshop on Computer Science Logic (CSL\u201990) . 95\u2013109. D. Cantone, V. Cutello, and J. T. Schwartz. 1990. Decision problems for Tarski\u2019s and Presburger\u2019s arithmetics extended with sets. In 3rd Workshop on Computer Science Logic (CSL\u201990). 95\u2013109."},{"key":"e_1_3_2_6_2","volume-title":"34th Italian Conference on Computational Logic. 123\u2013137","author":"Cantone D.","unstructured":"D. Cantone , A. De Domenico , P. Maugeri , and E. G. Omodeo . 2019. Polynomial-time satisfiability tests for Boolean fragments of set theory . In 34th Italian Conference on Computational Logic. 123\u2013137 . CEUR-WS.org. D. Cantone, A. De Domenico, P. Maugeri, and E. G. Omodeo. 2019. Polynomial-time satisfiability tests for Boolean fragments of set theory. In 34th Italian Conference on Computational Logic. 123\u2013137. CEUR-WS.org."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2021-2050"},{"key":"e_1_3_2_8_2","unstructured":"D. Cantone A. Ferro and E. G. Omodeo. 1989. Computable Set Theory(International Series of Monographs on Computer Science Vol. 6). Clarendon Press Oxford UK.  D. Cantone A. Ferro and E. G. Omodeo. 1989. Computable Set Theory (International Series of Monographs on Computer Science Vol. 6). Clarendon Press Oxford UK."},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1002\/cpa.3160380507","article-title":"Decision procedures for elementary sublanguages of set theory. VI. Multilevel syllogistic extended by the powerset operator","author":"Cantone D.","year":"1985","unstructured":"D. Cantone , A. Ferro , and J. T. Schwartz . 1985 . Decision procedures for elementary sublanguages of set theory. VI. Multilevel syllogistic extended by the powerset operator . Comm. Pure Appl. Math. XXXVIII , 1 (1985), 549 \u2013 571 . D. Cantone, A. Ferro, and J. T. Schwartz. 1985. Decision procedures for elementary sublanguages of set theory. VI. Multilevel syllogistic extended by the powerset operator. Comm. Pure Appl. Math. XXXVIII, 1 (1985), 549\u2013571.","journal-title":"Comm. Pure Appl. Math."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90001-8"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.08.023"},{"key":"e_1_3_2_12_2","volume-title":"22nd Italian Conference on Theoretical Computer Science (ICTCS\u201921)","author":"Cantone D.","unstructured":"D. Cantone , P. Maugeri , and E. G. Omodeo . 2021. Two crucial cubic-time components of polynomial-maximal decidable Boolean languages . In 22nd Italian Conference on Theoretical Computer Science (ICTCS\u201921) . CEUR-WS.org. D. Cantone, P. Maugeri, and E. G. Omodeo. 2021. Two crucial cubic-time components of polynomial-maximal decidable Boolean languages. In 22nd Italian Conference on Theoretical Computer Science (ICTCS\u201921). CEUR-WS.org."},{"key":"e_1_3_2_13_2","volume-title":"III: Testers for crucial, polynomial-maximal decidable Boolean languages. Theor. Comput. Sci. 954, 113786","author":"Cantone D.","year":"2023","unstructured":"D. Cantone , P. Maugeri , and E. G. Omodeo . 2023 . Complexity assessments for decidable fragments of set theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages. Theor. Comput. Sci. 954, 113786 (2023), 1\u201321. D. Cantone, P. Maugeri, and E. G. Omodeo. 2023. Complexity assessments for decidable fragments of set theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages. Theor. Comput. Sci. 954, 113786 (2023), 1\u201321."},{"key":"e_1_3_2_14_2","volume-title":"21st Italian Conference on Theoretical Computer Science (ICTCS\u201920)","author":"Cantone D.","unstructured":"D. Cantone , E. G. Omodeo , and M. Panettiere . 2020. From Hilbert\u2019s 10th problem to slim, undecidable fragments of set theory . In 21st Italian Conference on Theoretical Computer Science (ICTCS\u201920) . CEUR-WS.org. D. Cantone, E. G. Omodeo, and M. Panettiere. 2020. From Hilbert\u2019s 10th problem to slim, undecidable fragments of set theory. In 21st Italian Conference on Theoretical Computer Science (ICTCS\u201920). CEUR-WS.org."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245817"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"D. Cantone E. G. Omodeo and A. Policriti. 2001. Set Theory for Computing\u2014From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer-Verlag New York.  D. Cantone E. G. Omodeo and A. Policriti. 2001. Set Theory for Computing\u2014From Decision Procedures to Declarative Programming with Sets . Monographs in Computer Science. Springer-Verlag New York.","DOI":"10.1007\/978-1-4757-3452-2"},{"key":"e_1_3_2_17_2","volume-title":"Verification: Theory and Practice (Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday)","author":"Cantone D.","year":"2003","unstructured":"D. Cantone , E. G. Omodeo , J. T. Schwartz , and P. Ursino . 2003 . Notes from the logbook of a proof-checker\u2019s project. In Verification: Theory and Practice (Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday) . Springer-Verlag , Berlin , 182\u2013207. D. Cantone, E. G. Omodeo, J. T. Schwartz, and P. Ursino. 2003. Notes from the logbook of a proof-checker\u2019s project. In Verification: Theory and Practice (Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday). Springer-Verlag, Berlin, 182\u2013207."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3096"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.02.005"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","unstructured":"D. Cantone and P. Ursino. 2018. An Introduction to the Technique of Formative Processes in Set Theory.Springer International Publishing.  D. Cantone and P. Ursino. 2018. An Introduction to the Technique of Formative Processes in Set Theory. Springer International Publishing .","DOI":"10.1007\/978-3-319-74778-1"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.2307\/1970289"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpa.3160330503"},{"key":"e_1_3_2_23_2","first-page":"354","article-title":"Enumerable sets are Diophantine (in Russian)","volume":"11","author":"Matiyasevich Yu. V.","year":"2003","unstructured":"Yu. V. Matiyasevich . 2003 . Enumerable sets are Diophantine (in Russian) . Soviet Math. Doklady 11 , 2 (2003), 354 \u2013 358 . Yu. V. Matiyasevich. 2003. Enumerable sets are Diophantine (in Russian). Soviet Math. Doklady 11, 2 (2003), 354\u2013358.","journal-title":"Soviet Math. Doklady"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1902-00923-3"},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","unstructured":"E. G. Omodeo D. Cantone A. Policriti and J. T. Schwartz. 2006. A computerized referee. In Reasoning Action and Interaction in AI Theories and Systems \u2013 Essays dedicated to Luigia Carlucci Aiello. Springer Berlin 117\u2013139.  E. G. Omodeo D. Cantone A. Policriti and J. T. Schwartz. 2006. A computerized referee. In Reasoning Action and Interaction in AI Theories and Systems \u2013 Essays dedicated to Luigia Carlucci Aiello . Springer Berlin 117\u2013139.","DOI":"10.1007\/11829263_7"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"E. G. Omodeo A. Policriti and A. Tomescu. 2017. On Sets and Graphs: Perspectives on Logic and Combinatorics.Springer International Publishing.  E. G. Omodeo A. Policriti and A. Tomescu. 2017. On Sets and Graphs: Perspectives on Logic and Combinatorics. Springer International Publishing .","DOI":"10.1007\/978-3-319-54981-1"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","unstructured":"E. G. Omodeo and J. T. Schwartz. 2002. A \u201cTheory\u201d mechanism for a proof-verifier based on first-order set theory. In Computational Logic: Logic Programming and Beyond \u2013 Essays in honour of Bob Kowalski Part II. Springer-Verlag Berlin 214\u2013230.  E. G. Omodeo and J. T. Schwartz. 2002. A \u201cTheory\u201d mechanism for a proof-verifier based on first-order set theory. In Computational Logic: Logic Programming and Beyond \u2013 Essays in honour of Bob Kowalski Part II . Springer-Verlag Berlin 214\u2013230.","DOI":"10.1007\/3-540-45632-5_9"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1952-0048374-2"},{"key":"e_1_3_2_29_2","first-page":"93","article-title":"Complexity of subcases of Presburger","volume":"284","author":"Scarpellini B.","year":"1984","unstructured":"B. Scarpellini . 1984 . Complexity of subcases of Presburger Arithmetic. Trans. Am. Math. Soc. , 284 , I (1984), 93 \u2013 119 . B. Scarpellini. 1984. Complexity of subcases of Presburger Arithmetic. Trans. Am. Math. Soc., 284, I (1984), 93\u2013119.","journal-title":"Arithmetic. Trans. Am. Math. Soc."},{"key":"e_1_3_2_30_2","volume-title":"Instantiation and decision procedures for certain classes of quantified set-theoretic formulae. ICASE Rep. 78, 10","author":"Schwartz J. T.","year":"1978","unstructured":"J. T. Schwartz . 1978. Instantiation and decision procedures for certain classes of quantified set-theoretic formulae. ICASE Rep. 78, 10 ( 1978 ). J. T. Schwartz. 1978. Instantiation and decision procedures for certain classes of quantified set-theoretic formulae. ICASE Rep. 78, 10 (1978)."},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","unstructured":"J. T. Schwartz D. Cantone and E. G. Omodeo. 2011. Computational Logic and Set Theory: Applying Formalized Logic to Analysis. Springer-Verlag.  J. T. Schwartz D. Cantone and E. G. Omodeo. 2011. Computational Logic and Set Theory: Applying Formalized Logic to Analysis . Springer-Verlag.","DOI":"10.1007\/978-0-85729-808-9"},{"key":"e_1_3_2_32_2","volume-title":"I","author":"Ursino P.","year":"2005","unstructured":"P. Ursino . A generalized small model property for languages which force the infinity. Matematiche (Catania) LX , I ( 2005 ), 93\u2013119. P. Ursino. A generalized small model property for languages which force the infinity. Matematiche (Catania) LX, I (2005), 93\u2013119."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626823","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626823","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:15Z","timestamp":1750290255000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626823"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,16]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1,31]]}},"alternative-id":["10.1145\/3626823"],"URL":"https:\/\/doi.org\/10.1145\/3626823","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,16]]},"assertion":[{"value":"2021-05-07","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-27","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}