{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:42Z","timestamp":1749124062963},"publisher-location":"Berlin, Heidelberg","reference-count":12,"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_14","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"143-159","source":"Crossref","is-referenced-by-count":7,"title":["A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning"],"prefix":"10.1007","author":[{"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-61208-4_7","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"B. Beckert","year":"1996","unstructured":"Beckert, B., Pape, C.: Incremental theory reasoning methods for semantic ta- bleaux. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 93\u2013109. Springer, Heidelberg (1996)"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/164081.164101","volume-title":"Proceedings of 1993 Int. Symp. on Symbolic and Algebraic Computation, Kiev-Ukraine","author":"D. Cantone","year":"1993","unstructured":"Cantone, D., Cutello, V.: Decision procedures for stratified set-theoretic syllogi- stics. In: Proceedings of 1993 Int. Symp. on Symbolic and Algebraic Computation, Kiev-Ukraine, pp. 105\u2013110. ACM Press, New York (1993)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/3-540-54487-9_54","volume-title":"Computer Science Logic","author":"D. Cantone","year":"1991","unstructured":"Cantone, D., Cutello, V., Schwartz, J.T.: Decision problems for tarski\u2019s and presburger\u2019s arithmetics extended with sets. In: Sch\u00f6nfeld, W., B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1990. LNCS, vol.\u00a0533, pp. 95\u2013109. Springer, Heidelberg (1991)"},{"key":"14_CR4","first-page":"1","volume":"XLVIII","author":"D. Cantone","year":"1995","unstructured":"Cantone, D., Ferro, A.: Techniques of computable set theory with applications to proof verification. Comm. Pure Appl. Math.\u00a0XLVIII, 1\u201345 (1995)","journal-title":"Comm. Pure Appl. Math."},{"key":"14_CR5","series-title":"International 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. International Series of Monographs on Computer Science, vol.\u00a06. Clarendon Press, Oxford (1989)"},{"issue":"8","key":"14_CR6","doi-asserted-by":"publisher","first-page":"1175","DOI":"10.1002\/cpa.3160420809","volume":"XLII","author":"D. Cantone","year":"1989","unstructured":"Cantone, D., Omodeo, E.G.: Topological syllogistic with continuous and closed functions. Comm. Pure Appl. Math.\u00a0XLII(8), 1175\u20131188 (1989)","journal-title":"Comm. Pure Appl. Math."},{"key":"14_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-48754-9_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D. Cantone","year":"1999","unstructured":"Cantone, D., Zarba, C.G.: A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 97\u2013112. Springer, Heidelberg (1999)"},{"key":"14_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"127","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. 127\u2013137. Springer, Heidelberg (2000)"},{"key":"14_CR9","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 Publ. Comp. Inc., Reading (1979)"},{"key":"14_CR10","first-page":"130","volume":"33","author":"A. Ferro","year":"1978","unstructured":"Ferro, A., Omodeo, E.G.: An efficient validity test for formulae in extensional two-level syllogistic. Le Matematiche\u00a033, 130\u2013137 (1978)","journal-title":"Le Matematiche"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer, Heidelberg, 1st edn. (1990), 2nd edn. (1996)","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning\u00a01, 333\u2013355 (1985)","journal-title":"Journal of Automated Reasoning"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:09:19Z","timestamp":1553317759000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/10722086_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}