{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T05:27:55Z","timestamp":1769923675917,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540671909","type":"print"},{"value":"9783540465089","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_7","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:02:03Z","timestamp":1186171323000},"page":"109-125","source":"Crossref","is-referenced-by-count":2,"title":["A Further and Effective Liberalization of the \u03b4-Rule in Free Variable Semantic Tableaux"],"prefix":"10.1007","author":[{"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[]},{"given":"Marianna Nicolosi","family":"Asmundo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","volume-title":"4th International Workshop, TABLEAUX\u201995","author":"M. Baaz","year":"1995","unstructured":"M. Baaz, C.G. Ferm\u00fcller. Non-elementary speedups between different versions of tableaux. In 4th\n                           International Workshop, TABLEAUX\u201995 LNCS n. 918, 1995."},{"key":"7_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/BFb0022559","volume-title":"Computational Logic and Proof Theory","author":"B. Beckert","year":"1993","unstructured":"B. Beckert, R. H\u00e4hnle and P. Schmitt. The even more liberalized \u03b4-rule in free variable semantic tableaux. In Computational Logic and Proof Theory, Proceedings of the 3rd Kurt G\u00f6del Colloquium, Brno, August 1993. Springer, LNCS 713, pp. 108\u2013119."},{"key":"7_CR3","unstructured":"D. Cantone, M. Nicolosi Asmundo and E. Omodeo. Global Skolemization with grouped quantifiers. In Proceedings of APPIA-GULP PRODE\u201997: Joint Conference on Declarative Programming, pp. 405\u2013413, 1997."},{"issue":"14","key":"7_CR4","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1093\/logcom\/1.4.431","volume":"1","author":"M.D. Davis","year":"1991","unstructured":"M.D. Davis and R. Fechter. A free variable version of the first-order predicate calculus. Journal of Logic and Computation, 1(14):431\u2013451, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"7_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, New York, 1990."},{"issue":"2","key":"7_CR6","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle and P. Schmitt. The liberalized \u03b4-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211\u2013221, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. Smullyan","year":"1968","unstructured":"R. Smullyan. First-Order Logic. Springer, New York, 1968."}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T22:50:48Z","timestamp":1550443848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}