{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:02Z","timestamp":1749124082621},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:23:18Z","timestamp":1330251798000},"page":"57-71","source":"Crossref","is-referenced-by-count":20,"title":["The search efficiency of theorem proving strategies"],"prefix":"10.1007","author":[{"given":"David A.","family":"Plaisted","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Owen Astrachan and M. Stickel. Caching and lemma use in model elimination theorem provers. In D. Kapur, editor, Proceedings of the Eleventh International Conference on Automated Deduction, 1992.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"5_CR2","first-page":"427","volume-title":"On restrictions of ordered paramodulation with simplification","author":"L. Bachmair","year":"1990","unstructured":"Leo Bachmair and Harold Ganzinger. On restrictions of ordered paramodulation with simplification. In Mark Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 427\u2013441, New York, 1990. Springer-Verlag."},{"key":"5_CR3","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, Braunschweig\/Weisbaden, 1987. second edition.","edition":"second edition"},{"key":"5_CR4","volume-title":"The Computer Modelling of Mathematical Reasoning","author":"A. Bundy","year":"1983","unstructured":"A. Bundy. The Computer Modelling of Mathematical Reasoning. Academic Press, New York, 1983."},{"key":"5_CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973."},{"issue":"1","key":"5_CR6","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. A. Cook","year":"1979","unstructured":"S. A. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36\u201350, March 1979.","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-84222-0","volume-title":"Relative Complexities of First-Order Calculi","author":"E. Eder","year":"1992","unstructured":"E. Eder. Relative Complexities of First-Order Calculi. Vieweg, Braunschweig, 1992."},{"key":"5_CR9","doi-asserted-by":"crossref","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"},{"issue":"3","key":"5_CR10","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M Rusinowitch. Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method. J. Assoc. Comput. Mach., 38(3):559\u2013587, July 1991.","journal-title":"J. Assoc. Comput. Mach."},{"key":"5_CR11","unstructured":"H. Kleine Buening and T. Lettman. Search space and average proof length of resolution. Unpublished, 1993."},{"key":"5_CR12","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":"5_CR13","unstructured":"R. Letz. On the polynomial transparency of resolution. In Proceedings of the 13th International Joint Conference on Artificial Intelligence, pages 123\u2013129, 1993."},{"key":"5_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"J. W. Lloyd","year":"1987","unstructured":"J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. 2nd edn.","edition":"2nd edn"},{"key":"5_CR15","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. Loveland","year":"1969","unstructured":"D. Loveland. A simplified format for the model elimination procedure. J. ACM, 16:349\u2013363, 1969.","journal-title":"J. ACM"},{"key":"5_CR16","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"D. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland, New York, 1978."},{"issue":"1","key":"5_CR17","first-page":"25","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"S.-J. Lee and D. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1):25\u201342, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR18","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","volume":"18","author":"D. Plaisted","year":"1982","unstructured":"D. Plaisted. A simplified problem reduction format. Artificial Intelligence, 18:227\u2013261, 1982.","journal-title":"Artificial Intelligence"},{"key":"5_CR19","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"D. Plaisted. Non-Horn clause logic programming without contrapositives. Journal of Automated Reasoning, 4:287\u2013325, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR20","first-page":"227","volume":"1","author":"J. Robinson","year":"1965","unstructured":"J. Robinson. Automatic deduction with hyper-resolution. Int. J. Comput. Math., 1:227\u2013234, 1965.","journal-title":"Int. J. Comput. Math."},{"key":"5_CR21","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J. R. Slagle","year":"1967","unstructured":"J.R. Slagle. Automatic theorem proving with renameable and semantic resolution. J. ACM, 14:687\u2013697, 1967.","journal-title":"J. ACM"},{"key":"5_CR22","unstructured":"M.E. Stickel and W.M. Tyson. An analysis of consecutively bounded depth-first search with applications in automated deduction. In Proceedings of the 9th International Joint Conference on Artificial Intelligence, pages 1073\u20131075, 1985."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"T. Tammet. The resolution program: able to decide some solvable classes. In International Conference on Computer Logic, 1988, pages 300\u2013312, 1990. Springer Verlag LNCS 417.","DOI":"10.1007\/3-540-52335-9_61"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"T. Tammet. Using resolution for deciding solvable classes and building finite models. In Baltic Computer Science, pages 33\u201364, 1991. Springer Verlag LNCS 502.","DOI":"10.1007\/BFb0019355"},{"issue":"1","key":"5_CR25","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"A. Urquhart. Hard examples for resolution. J. ACM, 34(1):209\u2013219, 1987.","journal-title":"J. ACM"},{"key":"5_CR26","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1984","unstructured":"L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications. Prentice Hall, Englewood Cliffs, N.J., 1984."},{"key":"5_CR27","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. Robinson, and D. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the Association for Computing Machinery, 12:536\u2013541, 1965.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR28","first-page":"5","volume":"128","author":"N. K. Zamov","year":"1972","unstructured":"N.K. Zamov. On a bound for the complexity of terms in the resolution method. Trudy. Mat. Inst. Steklov, 128:5\u201313, 1972.","journal-title":"Trudy. Mat. Inst. Steklov"},{"key":"5_CR29","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0168-0072(89)90053-5","volume":"42","author":"N. K. Zamov","year":"1989","unstructured":"N.K. Zamov. Maslov's inverse method and decidable classes. Annals of pure and applied logic, 42:165\u2013194, 1989.","journal-title":"Annals of pure and applied logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:11:57Z","timestamp":1619557917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}