{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:39:51Z","timestamp":1750307991618,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2006,4,1]],"date-time":"2006-04-01T00:00:00Z","timestamp":1143849600000},"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":[[2006,4]]},"abstract":"<jats:p>\n            Formal set theory is traditionally concerned with\n            <jats:italic>pure<\/jats:italic>\n            sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called\n            <jats:italic>atoms<\/jats:italic>\n            ) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard extensionality axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms that allows one to retain the original formulation of extensionality was proposed by Quine: atoms are self-singletons. In this article we adopt this approach in coping with the satisfiability problem: We show the decidability of this problem relativized to \u2203*\u2200-sentences, and develop a goal-driven unification algorithm.\n          <\/jats:p>","DOI":"10.1145\/1131313.1131317","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:14:26Z","timestamp":1153836866000},"page":"269-301","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Decidability results for sets with atoms"],"prefix":"10.1145","volume":"7","author":[{"given":"Agostino","family":"Dovier","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Formisano","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di L'Aquila, L'Aquila, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eugenio G.","family":"Omodeo","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di L'Aquila, L'Aquila, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01594179"},{"key":"e_1_2_1_2_1","volume-title":"CSLI Lecture Notes","volume":"14","author":"Aczel P.","year":"1988","unstructured":"Aczel , P. 1988 . Non-Well-Founded Sets . CSLI Lecture Notes , vol. 14 , Stanford. Aczel, P. 1988. Non-Well-Founded Sets. CSLI Lecture Notes, vol. 14, Stanford."},{"key":"e_1_2_1_3_1","volume-title":"Foundations---Calculi and Methods","author":"Baader F.","year":"1998","unstructured":"Baader , F. and Schulz , K. U . 1998 . Unification theory. In Automated Deduction---A Basis for Applications, vol. I : Foundations---Calculi and Methods . W. Bibel and P. H. Schmidt, eds. Applied Logic Series, vol. 8. Kluwer Academic , Dordrecht, 225--263. Baader, F. and Schulz, K. U. 1998. Unification theory. In Automated Deduction---A Basis for Applications, vol. I: Foundations---Calculi and Methods. W. Bibel and P. H. Schmidt, eds. Applied Logic Series, vol. 8. Kluwer Academic, Dordrecht, 225--263."},{"key":"e_1_2_1_4_1","first-page":"445","article-title":"Unification theory. In Handbook of Automated Reasoning. A. Robinson and A. Voronkov, eds. Vol. I. Elsevier Science, Amsterdam","volume":"8","author":"Baader F.","year":"2001","unstructured":"Baader , F. and Snyder , W. 2001 . Unification theory. In Handbook of Automated Reasoning. A. Robinson and A. Voronkov, eds. Vol. I. Elsevier Science, Amsterdam , Chapter 8 , 445 -- 532 . Baader, F. and Snyder, W. 2001. Unification theory. In Handbook of Automated Reasoning. A. Robinson and A. Voronkov, eds. Vol. I. Elsevier Science, Amsterdam, Chapter 8, 445--532.","journal-title":"Chapter"},{"key":"e_1_2_1_5_1","volume-title":"Vicious Circles. CSLI Publication Notes","volume":"60","author":"Barwise J.","unstructured":"Barwise , J. and Moss , L . 1996 . Vicious Circles. CSLI Publication Notes , vol. 60 , Stanford. Barwise, J. and Moss, L. 1996. Vicious Circles. CSLI Publication Notes, vol. 60, Stanford."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881869"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of G\u00f6del'96-Logical Foundations of Mathematics, Computer Science and Physics-Kurt G\u00f6del's Legacy. Lecture Notes in Logic","volume":"6","author":"Bell\u00e8 D.","unstructured":"Bell\u00e8 , D. and Parlamento , F . 1995. Decidability of the &forall;&ast;&exist;&ast;-class in the membership theory nwl . In Proceedings of G\u00f6del'96-Logical Foundations of Mathematics, Computer Science and Physics-Kurt G\u00f6del's Legacy. Lecture Notes in Logic , vol. 6 . Springer Verlag, Berlin. Bell\u00e8, D. and Parlamento, F. 1995. Decidability of the &forall;&ast;&exist;&ast;-class in the membership theory nwl. In Proceedings of G\u00f6del'96-Logical Foundations of Mathematics, Computer Science and Physics-Kurt G\u00f6del's Legacy. Lecture Notes in Logic, vol. 6. Springer Verlag, Berlin."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80023-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245817"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Cantone D. Omodeo E. G. and Policriti A. 2001. Set Theory for Computing--From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer Verlag Berlin.   Cantone D. Omodeo E. G. and Policriti A. 2001. Set Theory for Computing--From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer Verlag Berlin.","DOI":"10.1007\/978-1-4757-3452-2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3096"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Doberkat E. E. and Fox D. 1989. Software Prototyping mit SETL. Leitfaden und Monographien der Informatik. B. G. Teubner Stuttgart.  Doberkat E. E. and Fox D. 1989. Software Prototyping mit SETL. Leitfaden und Monographien der Informatik. B. G. Teubner Stuttgart.","DOI":"10.1007\/978-3-322-94710-9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002000050109"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00147-6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/365151.365169"},{"key":"e_1_2_1_17_1","article-title":"Multiset rewriting by multiset constraint solving","volume":"4","author":"Dovier A.","year":"2001","unstructured":"Dovier , A. , Piazza , C. , and Rossi , G.-F. 2001 . Multiset rewriting by multiset constraint solving . Romanian J. Inf. Sci. Tech. 4 , 1\/2, 59--76. Dovier, A., Piazza, C., and Rossi, G.-F. 2001. Multiset rewriting by multiset constraint solving. Romanian J. Inf. Sci. Tech. 4, 1\/2, 59--76.","journal-title":"Romanian J. Inf. Sci. Tech."},{"key":"e_1_2_1_18_1","volume-title":"-F","author":"Dovier A.","year":"1998","unstructured":"Dovier , A. , Policriti , A. , and Rossi , G . -F . 1998 . A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundam. Inf ., 36, 2\/3, 201--234. Dovier, A., Policriti, A., and Rossi, G.-F. 1998. A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundam. Inf., 36, 2\/3, 201--234."},{"volume-title":"Elements of Set Theory","author":"Enderton H. B.","key":"e_1_2_1_19_1","unstructured":"Enderton , H. B. 1977. Elements of Set Theory . Academic Press , New York . Enderton, H. B. 1977. Elements of Set Theory. Academic Press, New York."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006437704595"},{"key":"e_1_2_1_21_1","volume-title":"Lecture Notes in Computer Science","volume":"2083","author":"Formisano A.","unstructured":"Formisano , A. , Omodeo , E. G. , and Temperini , M . 2001. Instructing equational set-reasoning with Otter. In Automated Reasoning. R. Gore, A. Leitsch, and T. Nipkow eds . Lecture Notes in Computer Science , vol. 2083 . Springer Verlag, Berlin, 152--167. Formisano, A., Omodeo, E. G., and Temperini, M. 2001. Instructing equational set-reasoning with Otter. In Automated Reasoning. R. Gore, A. Leitsch, and T. Nipkow eds. Lecture Notes in Computer Science, vol. 2083. Springer Verlag, Berlin, 152--167."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19780241902"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646523.694691"},{"key":"e_1_2_1_24_1","unstructured":"Hill P. and Lloyd J. 1994. The G\u00f6del Programming Language. MIT Press Cambridge MA.   Hill P. and Lloyd J. 1994. The G\u00f6del Programming Language. MIT Press Cambridge MA."},{"volume-title":"Set Theory. Pure and Applied Mathematics---A Series of Monographs and Textbooks","author":"Jech T.","key":"e_1_2_1_25_1","unstructured":"Jech , T. 1978. Set Theory. Pure and Applied Mathematics---A Series of Monographs and Textbooks , vol. 79 . Academic Press , New York . Jech, T. 1978. Set Theory. Pure and Applied Mathematics---A Series of Monographs and Textbooks, vol. 79. Academic Press, New York."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpa.3160480906"},{"volume-title":"Specifying Systems---The TLA&plus","author":"Lamport L.","key":"e_1_2_1_27_1","unstructured":"Lamport , L. 2002. Specifying Systems---The TLA&plus ; Language and Tools for Hardware and Software Engineers. Addison-Wesley , New York. Lamport, L. 2002. Specifying Systems---The TLA&plus; Language and Tools for Hardware and Software Engineers. Addison-Wesley, New York."},{"volume-title":"Basic Set Theory. Perspectives in Mathematical Logic","author":"Levy A.","key":"e_1_2_1_28_1","unstructured":"Levy , A. 1979. Basic Set Theory. Perspectives in Mathematical Logic . Springer Verlag , Berlin . Levy, A. 1979. Basic Set Theory. Perspectives in Mathematical Logic. Springer Verlag, Berlin."},{"key":"e_1_2_1_29_1","volume-title":"Tech. Rep. TR-96-5493-03b, ORA Canada.","author":"Meisels I.","year":"1996","unstructured":"Meisels , I. and Saaltink , M . 1996 . The Z\/EVES reference manual (for version 1.3). Tech. Rep. TR-96-5493-03b, ORA Canada. Meisels, I. and Saaltink, M. 1996. The Z\/EVES reference manual (for version 1.3). Tech. Rep. TR-96-5493-03b, ORA Canada."},{"key":"e_1_2_1_30_1","unstructured":"Mizar. Mizar Project Home Page. http:\/\/www.mizar.org.  Mizar. Mizar Project Home Page. http:\/\/www.mizar.org."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881863"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(06)80009-X"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19960420105"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpa.3160480908"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-97-03630-7"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881916"},{"key":"e_1_2_1_37_1","first-page":"23","article-title":"Generic automatic proof tools. In Automated Reasoning and Its Applications. R. Veroff., ed. MIT Press, Cambridge, MA","volume":"3","author":"Paulson L. C.","year":"1997","unstructured":"Paulson , L. C. 1997 . Generic automatic proof tools. In Automated Reasoning and Its Applications. R. Veroff., ed. MIT Press, Cambridge, MA , Chapter 3 , 23 -- 47 . Paulson, L. C. 1997. Generic automatic proof tools. In Automated Reasoning and Its Applications. R. Veroff., ed. MIT Press, Cambridge, MA, Chapter 3, 23--47.","journal-title":"Chapter"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00283132"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1693"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1995.1053"},{"volume-title":"Automated Development of Fundamental Mathematical Theories","author":"Quaife A.","key":"e_1_2_1_41_1","unstructured":"Quaife , A. 1992. Automated Development of Fundamental Mathematical Theories . Kluwer Academic , Dordrecht . Quaife, A. 1992. Automated Development of Fundamental Mathematical Theories. Kluwer Academic, Dordrecht."},{"volume-title":"Set Theory and its Logic","author":"Quine W. V.","key":"e_1_2_1_42_1","unstructured":"Quine , W. V. 1971. Set Theory and its Logic . Harvard University Press, Cambridge , MA. Quine, W. V. 1971. Set Theory and its Logic. Harvard University Press, Cambridge, MA."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/2215698.2215709"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/647282.722913"},{"key":"e_1_2_1_46_1","volume-title":"Sets: An Introduction to SETL. Texts and Monographs in Computer Science","author":"Schwartz J. T.","year":"1986","unstructured":"Schwartz , J. T. , Dewar , R. K. B. , Dubinsky , E. , and Schonberg , E . 1986 . Programming with Sets: An Introduction to SETL. Texts and Monographs in Computer Science . Springer Verlag , New York . Schwartz, J. T., Dewar, R. K. B., Dubinsky, E., and Schonberg, E. 1986. Programming with Sets: An Introduction to SETL. Texts and Monographs in Computer Science. Springer Verlag, New York."},{"key":"e_1_2_1_47_1","unstructured":"Setlog. The {log} Project Home Page. http:\/\/www.math.unipr.it\/~gianfr\/setlog.Home.html.  Setlog. The {log} Project Home Page. http:\/\/www.math.unipr.it\/~gianfr\/setlog.Home.html."},{"key":"e_1_2_1_48_1","unstructured":"SETS. The Programming with {SETS} Home Page. http:\/\/www.cs.nmsu.edu\/~complog\/sets.  SETS. The Programming with {SETS} Home Page. http:\/\/www.cs.nmsu.edu\/~complog\/sets."},{"key":"e_1_2_1_49_1","unstructured":"SICStus. Swedish Institute for Computer Science. Sicstus Prolog Home Page. http:\/\/www.sics.se\/sicstus.  SICStus. Swedish Institute for Computer Science. Sicstus Prolog Home Page. http:\/\/www.sics.se\/sicstus."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1131313.1131317","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1131313.1131317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:16Z","timestamp":1750259176000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1131313.1131317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["10.1145\/1131313.1131317"],"URL":"https:\/\/doi.org\/10.1145\/1131313.1131317","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,4]]},"assertion":[{"value":"2006-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}