{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:43Z","timestamp":1749124063038},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_29","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"368-382","source":"Crossref","is-referenced-by-count":2,"title":["Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory"],"prefix":"10.1007","author":[{"given":"Carla","family":"Piazza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Policriti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Aczel, P.: Non-Well-Founded Sets, CSLI Lecture Notes, vol.\u00a014 Stanford (1988)"},{"key":"29_CR2","unstructured":"Barwise, J., Moss, L.: Vicious circles, CSLI Public. Notes, vol.\u00a060 Stanford (1996)"},{"issue":"2","key":"29_CR3","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1093\/logcom\/7.2.251","volume":"7","author":"J.F.A.K. Benthem van","year":"1997","unstructured":"van Benthem, J.F.A.K., D\u2019Agostino, G., Montanari, A., Policriti, A.: Modal deduction in second-order logic and set theory-I. Journal of Logic and Computation\u00a07(2), 251\u2013265 (1997)","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"29_CR4","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1023\/A:1005037512998","volume":"60","author":"J.F.A.K. Benthem van","year":"1998","unstructured":"van Benthem, J.F.A.K., D\u2019 Agostino, G., Montanari, A., Policriti, A.: Modal deduction in second-order logic and set theory-II. Studia Logica\u00a060(3), 387\u2013420 (1998)","journal-title":"Studia Logica"},{"key":"29_CR5","volume-title":"Combinatorics","author":"B. Bollob\u00e1s","year":"1986","unstructured":"Bollob\u00e1s, B.: Combinatorics. Cambridge University Press, Cambridge (1986)"},{"key":"29_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The classical decision problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The classical decision problem. Springer, Heidelberg (1997)"},{"key":"29_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0027409","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D. Cantone","year":"1997","unstructured":"Cantone, D.: A fast saturation strategy for set-theoretic tableaux. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS (LNAI), vol.\u00a01227, pp. 122\u2013137. Springer, Heidelberg (1997)"},{"key":"29_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-46508-1_8","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D. Cantone","year":"2000","unstructured":"Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 126\u2013136. Springer, Heidelberg (2000)"},{"key":"29_CR9","series-title":"Int. Series of Monographs on Computer Science","volume-title":"Computable set theory","author":"D. Cantone","year":"1989","unstructured":"Cantone, D., Ferro, A., Omodeo, E.G.: Computable set theory. Int. Series of Monographs on Computer Science, vol.\u00a01. Oxford University Press, Oxford (1989)"},{"key":"29_CR10","unstructured":"Cantone, D., Omodeo, E.G., Ursino, P.: Transitive venn diagrams with applications to the decision problem in set theory. In: Meo, M.C. (ed.) Proc. APPIA GULP PRODE 1999 Joint Conference on Declarative Programming (1999)"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BF00881803","volume":"15","author":"G. D\u2019Agostino","year":"1996","unstructured":"D\u2019Agostino, G., Montanari, A., Policriti, A.: A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning\u00a015, 317\u2013337 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"29_CR12","volume-title":"The decision problem. solvable classes of quantificational formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D.: The decision problem. solvable classes of quantificational formulas. Addison-Wesley, Reading (1979)"},{"key":"29_CR13","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"33","author":"A. Ferro","year":"1980","unstructured":"Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision Procedures for Elementary Sublanguages of Set Theory I. Multilevel Syllogistic and Some Extensions. Comm. Pure App. Math.\u00a033, 599\u2013608 (1980)","journal-title":"Comm. Pure App. Math."},{"issue":"10","key":"29_CR14","first-page":"493","volume":"IV","author":"M. Forti","year":"1983","unstructured":"Forti, M., Honsell, F.: Set theory with free construction principles. Annali Scuola Normale Superiore di Pisa, Cl. Sc\u00a0IV(10), 493\u2013522 (1983)","journal-title":"Annali Scuola Normale Superiore di Pisa, Cl. Sc"},{"key":"29_CR15","volume-title":"Unsolvable classes of quantificational formulas","author":"H.R. Lewis","year":"1979","unstructured":"Lewis, H.R.: Unsolvable classes of quantificational formulas. Addison-Wesley, Reading (1979)"},{"issue":"9-10","key":"29_CR16","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1002\/cpa.3160480908","volume":"48","author":"E.G. Omodeo","year":"1995","unstructured":"Omodeo, E.G., Policriti, A.: Solvable set\/hyperset contexts: I. Some decision procedures for the pure, finite case. Comm. Pure App. Math.\u00a048(9-10), 1123\u20131155 (1995); Special Issue in honor of J.T. Schwartz","journal-title":"Comm. Pure App. Math."},{"key":"29_CR17","unstructured":"Parlamento, F., Policriti, A., Rao, K.P.S.B.: Witnessing Differences Without Redundancies, Tech. Report 23\/93, Universit\u00e0 di Udine (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T09:17:34Z","timestamp":1553332654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10722086_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}