{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:22:01Z","timestamp":1760016121408},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_97","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:34Z","timestamp":1330293034000},"page":"313-327","source":"Crossref","is-referenced-by-count":25,"title":["Optimizing proof search in model elimination"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"34_CR1","doi-asserted-by":"crossref","unstructured":"O. L. Astrachan and M. E. Stickel. Caching and lemmaizing in model elimination theorem provers. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, pages 224\u2013238, 1992. Springer-Verlag.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"34_CR2","unstructured":"P. Baumgartner and U. Furbach. Model elimination without contrapositives and its application to PTTP. Research report 12-93, Institute for Computer Science, University of Koblenz, 1993."},{"key":"34_CR3","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"B. Beckert and J. Posegga. leanT A P: Lean, tableau-based deduction. Journal of Automated Reasoning, 15:339\u2013358, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR4","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"34_CR5","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":"34_CR6","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, and W. Bibel. SETHEO: A high-performance theorem proven. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled integrations of the cut rule into connection tableau calculi. Technical Report AR-94-01, TU M\u00fcnchen, 1994.","DOI":"10.1007\/BF00881947"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"V. Lifschitz. Mechanical Theorem Proving in the USSR: the Leningrad School. Monograph Series on Soviet Union. Delphic Associates, 1986. See also \u2018What is the inverse method?\u2019 in the Journal of Automated Reasoning, vol. 5, pp. 1\u201323, 1989.","DOI":"10.1007\/BF00245018"},{"key":"34_CR9","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:236\u2013251, 1968.","journal-title":"Journal of the ACM"},{"key":"34_CR10","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1038\/218019a0","volume":"218","author":"D. Michie","year":"1968","unstructured":"D. Michie. \u201cMemo\u201d functions and machine learning. Nature, 218:19\u201322, 1968.","journal-title":"Nature"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994. With contributions by Tobias Nipkow.","DOI":"10.1007\/BFb0030541"},{"key":"34_CR12","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/BF00244355","volume":"6","author":"D. A. Plaisted","year":"1990","unstructured":"D. A. Plaisted. A sequent-style model elimination strategy and a positive refinement. Journal of Automated Reasoning, 6:389\u2013402, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR13","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"P. Rudnicki. Obvious inferences. Journal of Automated Reasoning, 3:383\u2013393, 1987.","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR14","doi-asserted-by":"publisher","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"},{"key":"34_CR15","unstructured":"C. B. Suttner and G. Sutcliffe. The TPTP problem library. Technical Report AR-95-03, TU M\u00fcnchen, 1995."},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"M. Tarver. An examination of the Prolog Technology Theorem-Prover. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 322\u2013335, 1990. Springer-Verlag.","DOI":"10.1007\/3-540-52885-7_97"},{"key":"34_CR17","unstructured":"P. Weis and X. Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http:\/\/pauillac.inria.fr\/caml\/."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_97.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:40:49Z","timestamp":1640947249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_97"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_97","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}