{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:17:13Z","timestamp":1759637833767},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_8","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:02:03Z","timestamp":1186171323000},"page":"126-136","source":"Crossref","is-referenced-by-count":8,"title":["A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory"],"prefix":"10.1007","author":[{"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-69778-0_16","volume-title":"Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands","author":"B. Beckert","year":"1998","unstructured":"Bernhard Beckert and Ulrike Hartmer. A tableau calculus for quantifier-free set theoretic formulae. In Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, LNCS 1397, pages 93\u2013107. Springer, 1998."},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-61474-5_92","volume-title":"Proc. 8thIntl. Conference on Computer Aided Verification","author":"N. S. Bj\u00f8rner","year":"1996","unstructured":"Nikolaj S. Bj\u00f8rner, Anca Browne, Eddie S. Chang, Michael Col\u00f3n, Arjun Kapur, Zohar Manna, Henny B. Sipma, and Tom\u00e1s E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Proc. 8th\n                           Intl. Conference on Computer Aided Verification, volume 1102 of LNCS, pages 415\u2013418. Springer-Verlag, July 1996."},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-63104-6_13","volume-title":"Proc. of the 14thIntl. Conference on Automated Deduction","author":"N. S. Bj\u00f8rner","year":"1997","unstructured":"Nikolaj S. Bj\u00f8rner, Mark E. Stickel, and Tom\u00e1s E. Uribe. A practical integration of first-order reasoning and decision procedures. In Proc. of the 14th\n                           Intl. Conference on Automated Deduction, volume 1249 of LNCS, pages 101\u2013115. Springer-Verlag, July 1997."},{"doi-asserted-by":"crossref","unstructured":"Domenico Cantone. A fast saturation strategy for set-theoretic Tableaux. In Didier Galmiche, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 1227 of LNAI, pages 122\u2013137, Berlin, May 13\u201316 1997. Springer.","key":"8_CR4","DOI":"10.1007\/BFb0027409"},{"key":"8_CR5","first-page":"1","volume":"XLVIII","author":"D. Cantone","year":"1995","unstructured":"Domenico Cantone and Alfredo Ferro. Techniques of computable set theory with applications to proof verification. Comm. Pure Appl. Math., XLVIII:1\u201345, 1995.","journal-title":"Comm. Pure Appl. Math."},{"unstructured":"Domenico Cantone, Alfredo Ferro, and Eugenio Omodeo. Computable set theory, volume no.6 Oxford Science Publications of International Series of Monographs on Computer Science. Clarendon Press, 1989.","key":"8_CR6"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M. D\u2019Agostino","year":"1994","unstructured":"Marcello D\u2019Agostino and Marco Mondadori. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation, 4(3):285\u2013319, June 1994.","journal-title":"Journal of Logic and Computation"},{"key":"8_CR8","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. C. Fitting","year":"1996","unstructured":"Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer-Verlag, Berlin, 2nd edition, 1996. 1st ed., 1990.","edition":"2nd edition"},{"unstructured":"Calogero G. Zarba. Dimostrazione automatica di formule inisiemistiche con tagli analitici. Tesi di Laurea, Universit\u00e0 di Catania (in Italian), July 1998.","key":"8_CR9"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,20]],"date-time":"2019-02-20T22:49:50Z","timestamp":1550702990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}