{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:40Z","timestamp":1760202520574},"publisher-location":"Berlin\/Heidelberg","reference-count":8,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022559","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:14:45Z","timestamp":1131862485000},"page":"108-119","source":"Crossref","is-referenced-by-count":20,"title":["The even more liberalized \u03b4-rule in free variable Semantic Tableaux"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter H.","family":"Schmitt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory. Academic Press, 1986."},{"key":"13_CR2","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. C. Fitting","year":"1988","unstructured":"Melvin C. Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191\u2013213, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. C. Fitting","year":"1990","unstructured":"Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, New York, 1990."},{"key":"13_CR4","unstructured":"Reiner H\u00e4hnle. Automated Theorem Proving in Multiple-Valued Logics. Oxford University Press, forthcoming, 1993."},{"key":"13_CR5","unstructured":"Reiner H\u00e4hnle, Bernhard Beckert, Stefan Gerberding, and Werner Kernig. The Many-Valued Tableau-Based Theorem Prover 3TAP. IWBS Report 227, Wissenschaftliches Zentrum Heidelberg, IWBS, IBM Deutschland, July 1992."},{"key":"13_CR6","unstructured":"Reiner H\u00e4hnle and Peter H. Schmitt. The liberalized \u03b4-rule in free variable semantic tableaux. Journal of Automated Reasoning, to appear, 1993."},{"key":"13_CR7","unstructured":"Steve V. Reeves. Semantic tableaux as a framework for automated theorem-proving. Department of Computer Science and Statistics, Queen Mary College, Univ. of London, 1987."},{"key":"13_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. Smullyan","year":"1968","unstructured":"Raymond Smullyan. First-Order Logic. Springer, New York, 1968."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022559.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:49:00Z","timestamp":1607550540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022559"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0022559","relation":{},"subject":[]}}