{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:34Z","timestamp":1725663634202},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569442"},{"type":"electronic","value":"9783540478300"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56944-8_55","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T06:57:48Z","timestamp":1330239468000},"page":"217-228","source":"Crossref","is-referenced-by-count":3,"title":["Refinements and extensions of model elimination"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Mayr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"O. L. Astrachan and M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In Automated Deduction CADE-11, pages 222\u2013238, June 1992.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"19_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987.","edition":"second edition"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift, 39:176\u2013210 and 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"19_CR4","unstructured":"A. Goerdt. Regular Resolution versus Unrestricted Resolution. Technical report, Universit\u00e4t Duisburg, 1989. to appear in SIAM Journal of Computing."},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken. The Intractability of Resolution. Theoretical Computer Science, 39:297\u2013308, 1985.","journal-title":"Theoretical Computer Science"},{"key":"19_CR6","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"R. E. Korf. Depth-first Iterative Deepening: an Optimal Admissible Tree Search. Artificial Intelligence, 27:97\u2013109, 1985.","journal-title":"Artificial Intelligence"},{"key":"19_CR7","volume-title":"PhD thesis","author":"R. Letz","year":"1993","unstructured":"R. Letz. First Order Calculi and Proof Procedures. PhD thesis, Technische Universit\u00e4t M\u00fcnchen \/ Darmstadt, April 1993."},{"issue":"2","key":"19_CR8","doi-asserted-by":"crossref","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 Association for Computing Machinery, 15(2):236\u2013251, 1968.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"19_CR9","unstructured":"D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. A High Performance Theorem Prover. Journal of Automated Reasoning, August 1992.","DOI":"10.1007\/BF00244282"},{"key":"19_CR11","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/BFb0060631","volume":"125","author":"D. Luckham","year":"1970","unstructured":"D. Luckham. Refinement Theorems in Resolution Theory. In Symposium on Automatic Demonstration, volume 125, pages 163\u2013190. Lecture Notes on Mathematics, 1970.","journal-title":"Symposium on Automatic Demonstration"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"K. Mayr. Refinements and Extensions of Model Elimination. Technical report, Technische Universit\u00e4t M\u00fcnchen, April 1993.","DOI":"10.1007\/3-540-56944-8_55"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"R. M. Smullyan. First Order Logic. Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"G. S. Tseitin. On the Length of Derivations in the Propositional Calculus. In Studies in Mathematics and Mathematical Logic II, pages 115\u2013125. A. O. Slsenko, 1970.","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56944-8_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:07:42Z","timestamp":1605629262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56944-8_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569442","9783540478300"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-56944-8_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}