{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:20:31Z","timestamp":1758979231252,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054273","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"381-396","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Using matings for pruning connection tableaux"],"prefix":"10.1007","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"issue":"2","key":"34_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"P. Andrews. Theorem Proving via General Matings. Journal of the Association for Computing Machinery, 28(2):193\u2013214, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"O. W. Astrachan and M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. Proceedings of the 11th Conference on Automated Deduction (CADE-11), LNAI 607, pages 224\u2013238, Springer, 1992.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"34_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On Matrices withConnections. Journal of the ACM, 28:633\u2013645, 1981.","journal-title":"Journal of the ACM"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"34_CR5","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving, Springer, 2nd edition, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"34_CR6","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0004-3702(96)00046-X","volume":"92","author":"J. D. Horton","year":"1997","unstructured":"J. D. Horton and B. Spencer. Clause trees: a tool for understanding and implementing resolution in automated deduction. Artificial Intelligence, 92:25\u201389, 1997.","journal-title":"Artificial Intelligence"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"O. Ibens and R. Letz. Subgoal Alternation in Model Elimination. In Proceedings of TABLEAUX'97, LNAI 1227, pages 201\u2013215, Springer, 1997.","DOI":"10.1007\/BFb0027415"},{"key":"34_CR8","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R. A. Kowalski","year":"1970","unstructured":"R. A. Kowalski and D. Kuehner. Linear Resolution with Selection Function. Artificial Intelligence, 2:227\u2013260, 1970.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"34_CR9","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2):183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR10","unstructured":"R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, Technische Hochschule Darmstadt, 1993 (http:\/\/wwwjessen.informatik.tu-muenchen.de\/personen\/letz.html)."},{"key":"34_CR11","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableaux Calculi. Journal of Automated Reasoning, 13:297\u2013337, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR12","unstructured":"R. Letz. Clausal Tableaux. In W. Bibel, P. H. Schmitt, editors, Automated Deduction. A basis for applications, Vol. 1, pages 39\u201368, Kluwer, 1998."},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"R. Letz. First-order Tableau Methods. In M. D'Agostino, D. Gabbay, R. H\u00c4hnle, J. Posegga, editors, Handbook of Tableau Methods, Kluwer, 1998.","DOI":"10.1007\/978-94-017-1754-0_3"},{"issue":"2","key":"34_CR14","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1968","unstructured":"D. W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15(2):236\u2013251, 1968.","journal-title":"Journal of the ACM"},{"key":"34_CR15","unstructured":"D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978."},{"key":"34_CR16","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, K. Mayr. SETHEO and E-SETHEO. Journal of Automated Reasoning, 18:237\u2013246, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR17","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"D. Prawitz. An Improved Proof Procedure. Theoria, 26:102\u2013139, 1960.","journal-title":"Theoria"},{"key":"34_CR18","unstructured":"S. Reeves. Semantic tableaux as a framework for automated theorem-proving. In C. S. Mellish and J. Hallam, editors, Advances in Artificial Intelligence (Proceedings of AISB-87), pages 125\u2013139, Wiley, 1987."},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"R. M. Smullyan. First-Order Logic. Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"34_CR20","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. A. Stickel","year":"1988","unstructured":"M. A. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054273","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T21:17:13Z","timestamp":1674163033000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054273"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0054273","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}