{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:24:42Z","timestamp":1725456282634},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540629207"},{"type":"electronic","value":"9783540690467"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027415","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:34:36Z","timestamp":1132641276000},"page":"201-215","source":"Crossref","is-referenced-by-count":8,"title":["Subgoal alternation in model elimination"],"prefix":"10.1007","author":[{"given":"Ortrun","family":"Ibens","sequence":"first","affiliation":[]},{"given":"Reinhold","family":"Letz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"O. L. Astrachan, M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. CADE-11, LNAI 607, p. 224\u2013238, Springer, 1992.","key":"15_CR1","DOI":"10.1007\/3-540-55602-8_168"},{"issue":"4","key":"15_CR2","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving theorems with the modification method. SIAM Journal of Computing, 4(4):412\u2013430, 1975.","journal-title":"SIAM Journal of Computing"},{"doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving, Springer, 1990.","key":"15_CR3","DOI":"10.1007\/978-1-4684-0357-2"},{"doi-asserted-by":"crossref","unstructured":"C. Goller, R. Letz, K. Mayr, J. Schumann. SETHEO V3.2: Recent Developments-System Abstract-.CADE-12, LNAI 814, p. 778\u2013782, Springer, 1994.","key":"15_CR4","DOI":"10.1007\/3-540-58156-1_59"},{"doi-asserted-by":"crossref","unstructured":"J. Harrison. Optimizing proof search in model elimination. GADE-13, LNAI 1104, p. 313\u2013327, Springer, 1996.","key":"15_CR5","DOI":"10.1007\/3-540-61511-3_97"},{"unstructured":"R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. Dissertation, Technische Hochschule Darmstadt, 1993.","key":"15_CR6"},{"key":"15_CR7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR8","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13:297\u2013337, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR9","volume-title":"Automated theorem proving: A logical basis","author":"D. W. Loveland","year":"1978","unstructured":"D. W. Loveland. Automated theorem proving: A logical basis. North Holland, New York, 1978."},{"unstructured":"M. Moser, C. Lynch, J. Steinbach. Model elimination with basic ordered paramodulation. Technical Report AR-95-11, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1995.","key":"15_CR10"},{"unstructured":"M. Moser. Goal-directed reasoning in clausal logic with equality. Dissertation, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1996.","key":"15_CR11"},{"unstructured":"M. Moser. Compiling basic paramodulation to logic. Technical report, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1997.","key":"15_CR12"},{"unstructured":"M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, K. Mayr. SETHEO and E-SETHEO. Special issue of the Journal of Automated Reasoning, to appear 1997.","key":"15_CR13"},{"key":"15_CR14","first-page":"135","volume":"4","author":"G. A. Robinson","year":"1969","unstructured":"G. A. Robinson, L. Wos. Paramodulation and theorem proving in first-order theories with equality. Machine Intelligence, 4:135\u2013150, 1969.","journal-title":"Machine Intelligence"},{"key":"15_CR15","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"R. E. Shostak. Refutation graphs. Artificial Intelligence, 7:51\u201364, 1976.","journal-title":"Artificial Intelligence"},{"key":"15_CR16","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"M. E. 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"},{"doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. B. Suttner, T. Yemenis. The TPTP problem library. CADE-12, LNAI 814 of, p. 778\u2013782, Springer, 1994.","key":"15_CR17","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027415","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:46:38Z","timestamp":1586573198000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027415"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540629207","9783540690467"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0027415","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}