{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T22:16:42Z","timestamp":1649197002920},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10817-004-8271-4","type":"journal-article","created":{"date-parts":[[2005,4,20]],"date-time":"2005-04-20T13:42:35Z","timestamp":1114004555000},"page":"49-72","source":"Crossref","is-referenced-by-count":2,"title":["A Tableau-Based Decision Procedure for a Fragment of Set Theory with Iterated Membership"],"prefix":"10.1007","volume":"34","author":[{"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]},{"given":"Rosa Ruggeri","family":"Cannata","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","volume-title":"Non-Well-Founded Sets","author":"P. Aczel","year":"1988","unstructured":"Aczel, P.: Non-Well-Founded Sets, CSLI Publications, Stanford, CA, 1988."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Cantone, D.: A fast saturation strategy for set-theoretic tableaux, in D. Galmiche (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Comput. Sci. 1227, Springer, 1997, pp. 122?137.","DOI":"10.1007\/BFb0027409"},{"key":"CR3","unstructured":"Cantone, D. and Cincotti, G.: The decision problem in graph theory with reachability related constructs, in P. Baumgartner and H. Zhang (eds.), Third International Workshop on First-Order Theorem Proving (FTP 2000), Technical Report 5\/2000, Universit\u00e4t Koblenz-Landau, 2000, pp. 68?80."},{"issue":"9?10","key":"CR4","first-page":"1","volume":"48","author":"D. Cantone","year":"1995","unstructured":"Cantone, D. and Ferro, A.: Techniques of computable set theory with applications to proof verification, Comm. Pure Appl. Math. 48(9?10) (1995), 1?45.","journal-title":"Comm. Pure Appl. Math."},{"key":"CR5","unstructured":"Cantone, D., Ferro, A. and Omodeo, E. G.: Computable Set Theory, Internat. Ser. Monographs Comput. Sci. 6, Clarendon Press, 1989."},{"issue":"2","key":"CR6","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF00245817","volume":"6","author":"D. Cantone","year":"1990","unstructured":"Cantone, D., Omodeo, E. G. and Policriti, A.: The automation of syllogistic, II: Optimization and complexity issues, J. Automated Reasoning 6(2) (1990), 173?187.","journal-title":"J. Automated Reasoning"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Cantone, D., Omodeo, E. G. and Policriti, A.: Set Theory for Computing: From Decision Procedures to Logic Programming with Sets, Monographs in Computer Science, Springer, 2001.","DOI":"10.1007\/978-1-4757-3452-2"},{"issue":"I","key":"CR8","first-page":"99","volume":"L","author":"D. Cantone","year":"1995","unstructured":"Cantone, D. and Cannata, R. R.: Deciding set-theoretic formulae with the predicate Finite by a tableau calculus, Le Matematiche L(I) (1995), 99?118.","journal-title":"Le Matematiche"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Cantone, D. and Zarba, C. G.: A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification, in N. V. Murray (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Comput. Sci. 1617, Springer, 1999, pp. 97?112.","DOI":"10.1007\/3-540-48754-9_12"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Cantone, D. and Zarba, C. G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory, in R. Caferra and G. Salzer (eds.), Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Comput. Sci. 1761, Springer, 2000, pp. 127?137.","DOI":"10.1007\/3-540-46508-1_8"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Cantone, D. and Zarba, C. G.: A tableau calculus for integrating first-order reasoning with elementary set theory reasoning, in R. Dyckhoff (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Comput. Sci. 1847, Springer, 2000, pp. 143?159.","DOI":"10.1007\/10722086_14"},{"issue":"5","key":"CR12","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"33","author":"A. Ferro","year":"1980","unstructured":"Ferro, A., Omodeo, E. G. and Schwartz, J. T.: Decision procedures for elementary sublanguages of set theory, I: Multi-level syllogistic and some extensions, Comm. Pure Appl. Math. 33(5) (1980), 599?608.","journal-title":"Comm. Pure Appl. Math."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Fitting, M. C.: First-Order Logic and Automated Theorem Proving, 2nd edn, Graduate Texts in Computer Science, Springer, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Piazza, C. and Policriti, A.: Towards tableau-based decision procedures for non-well-founded fragments of set theory, in R. Dyckhoff (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Comput. Sci. 1847, Springer, 2000, pp. 368?382.","DOI":"10.1007\/10722086_29"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Smullyan, R. M.: First-Order Logic, Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"CR16","unstructured":"Zarba, C. G.: Combining sets with elements, in N. Dershowitz (ed.), Verification: Theory and Practice, Lecture Notes in Comput. Sci. 2772, Springer, 2004, pp. 762?782."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-8271-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-8271-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-8271-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:45Z","timestamp":1559251305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-8271-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["8271"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-8271-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1]]}}}