{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T08:22:04Z","timestamp":1760170924461,"version":"3.41.0"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_1","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"3-28","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["History and Prospects for First-Order Automated Deduction"],"prefix":"10.1007","author":[{"given":"David A.","family":"Plaisted","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P Andrews","year":"1981","unstructured":"Andrews, P.: Theorem proving via general matings. J. ACM 28, 193\u2013214 (1981)","journal-title":"J. ACM"},{"key":"1_CR2","series-title":"Rewriting Techniques","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures Progress in Theoretical Computer Science","author":"L Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.: Completion without failure. In: Kaci, H.A., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures Progress in Theoretical Computer Science. Rewriting Techniques, vol. 2, pp. 1\u201330. Academic Press, New York (1989)"},{"key":"1_CR3","first-page":"3","volume-title":"Machine Intelligence","author":"A Ballantyne","year":"1982","unstructured":"Ballantyne, A., Bledsoe, W.: On generating and using examples in proof discovery. In: Hayes, J., Michie, D., Pao, Y.H. (eds.) Machine Intelligence, vol. 10, pp. 3\u201339. Ellis Horwood, Chichester (1982)"},{"issue":"1","key":"1_CR4","first-page":"35","volume":"24","author":"P Baumgartner","year":"2010","unstructured":"Baumgartner, P., Thorstensen, E.: Instance based methods - a brief overview. Ger. J. Artif. Intell. (KI) 24(1), 35\u201342 (2010)","journal-title":"Ger. J. Artif. Intell. (KI)"},{"issue":"4\u20135","key":"1_CR5","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1016\/j.artint.2007.09.005","volume":"172","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4\u20135), 591\u2013632 (2008)","journal-title":"Artif. Intell."},{"key":"1_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-90100-2","volume-title":"Automated Theorem Proving","author":"W Bibel","year":"1982","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg, Braunschweig (1982)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"JP Billon","year":"1996","unstructured":"Billon, J.P.: The disconnection method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"WW Bledsoe","year":"1977","unstructured":"Bledsoe, W.W.: Non-resolution theorem proving. Artif. Intell. 9(1), 1\u201335 (1977)","journal-title":"Artif. Intell."},{"key":"1_CR9","unstructured":"Bledsoe, W.W.: Using examples to generate instantiations of set variables. In: Proceedings of the 8th International Joint Conference on Artificial Intelligence, pp. 892\u2013901. William Kaufmann (1983)"},{"key":"1_CR10","series-title":"Contemporary mathematics","volume-title":"Automated Theorem Proving: After 25 Years","year":"1984","unstructured":"Bledsoe, W.W., Loveland, D.W. (eds.): Automated Theorem Proving: After 25 Years. Contemporary mathematics. American Mathematical Society, Providence (1984)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: On first-order model-based reasoning. In: Mart\u00ed-Oliet, N., Olveczky, P., Talcott, C. (eds.) Logic, Rewriting, and Concurrency: Essays in Honor of Jos\u00e9 Meseguer. LNCS, vol. 9200, Springer, Heidelberg (2015, to appear)","DOI":"10.1007\/978-3-319-23165-5_8"},{"key":"1_CR12","unstructured":"Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Konev, B., Moura, L.D., Schulz, S. (eds.) Proceedings of the 4th Workshop on Practical Aspects in Automated Reasoning, EasyChair Proceedings in Computing (2014, to appear)"},{"key":"1_CR13","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C Chang","year":"1973","unstructured":"Chang, C., Lee, R.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-58156-1_14","volume-title":"Automated Deduction - CADE-12","author":"H Chu","year":"1994","unstructured":"Chu, H., Plaisted, D.: Semantically guided first-order theorem proving using hyper-linking. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 192\u2013206. Springer, Heidelberg (1994)"},{"key":"1_CR15","unstructured":"Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality (2005). Presented at Dagstuhl Seminar on Deduction and Applications"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Davis, M.: Eliminating the irrelevant from machanical proofs. In: Proceedings of Symposia in Applied Mathematics, vol. 15, pp. 15\u201330 (1963)","DOI":"10.1090\/psapm\/015\/0170497"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279\u2013301 (1982)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"1_CR20","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00161-X","volume":"265","author":"O Dubois","year":"2001","unstructured":"Dubois, O.: Upper bounds on the satisfiability threshold. Theor. Comput. Sci. 265(1\u20132), 187\u2013197 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR21","volume-title":"Computers and Thought","author":"EA Feigenbaum","year":"1963","unstructured":"Feigenbaum, E.A., Feldman, J.: Computers and Thought. McGraw-Hill, New York (1963)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-45085-6_27","volume-title":"Automated Deduction \u2013 CADE-19","author":"J-M Gaillourdet","year":"2003","unstructured":"Gaillourdet, J.-M., Hillenbrand, T., L\u00f6chner, B., Spies, H.: The new WALDMEISTER loop at work. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 317\u2013321. Springer, Heidelberg (2003)"},{"key":"1_CR23","first-page":"153","volume-title":"Computers and Thought","author":"H Gelernter","year":"1963","unstructured":"Gelernter, H., Hansen, J., Loveland, D.: Empirical explorations of the geometry theorem proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp. 153\u2013167. McGraw-Hill, New York (1963)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"1","key":"1_CR25","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"PC Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory. IBM J. Res. Dev. 4(1), 28\u201335 (1960)","journal-title":"IBM J. Res. Dev."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Green, C.: Application of theorem proving to problem solving. In: Proceedings of the 1st International Joint Conference on Artificial Intelligence, pp. 219\u2013239. Morgan Kaufmann (1969)","DOI":"10.21236\/ADA459656"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BFb0000058","volume-title":"6th Conference on Automated Deduction","author":"S Greenbaum","year":"1982","unstructured":"Greenbaum, S., Nagasaka, A., O\u2019Rorke, P., Plaisted, D.A.: Comparison of natural deduction and locking resolution implementations. In: Loveland, D. (ed.) 6th Conference on Automated Deduction. LNCS, vol. 138, pp. 159\u2013171. Springer, Heidelberg (1982)"},{"key":"1_CR28","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal Language Theory: Perspectives and Open Problems","author":"G Huet","year":"1980","unstructured":"Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349\u2013405. Academic Press, New York (1980)"},{"key":"1_CR29","unstructured":"Iturriaga, R.: Contributions to mechanical mathematics. Ph.D. thesis, Carnegie-Mellon University, Pittsburgh, Pennsylvania (1967)"},{"key":"1_CR30","unstructured":"Jefferson, S., Plaisted, D.: Implementation of an improved relevance criterion. In: Proceedings of the 1st Conference on Artificial Intelligence Applications, pp. 476\u2013482. IEEE Computer Society Press (1984)"},{"issue":"1","key":"1_CR31","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W Joyner","year":"1976","unstructured":"Joyner, W.: Resolution strategies as decision procedures. J. ACM 23(1), 398\u2013417 (1976)","journal-title":"J. ACM"},{"key":"1_CR32","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-14203-1_17","volume-title":"Automated Reasoning","author":"K Korovin","year":"2010","unstructured":"Korovin, K., Sticksel, C.: iProver-eq: an instantiation-based theorem prover with equality. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 196\u2013202. Springer, Heidelberg (2010)"},{"key":"1_CR34","unstructured":"Lankford, D.: Canonical algebraic simplification in computational logic. Technical report, Memo ATP-25, University of Texas, Austin, Texas (1975)"},{"issue":"1","key":"1_CR35","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"SJ Lee","year":"1992","unstructured":"Lee, S.J., Plaisted, D.: Eliminating duplication with the hyper-linking strategy. J. Autom. Reasoning 9(1), 25\u201342 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR36","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D Loveland","year":"1969","unstructured":"Loveland, D.: A simplified format for the model elimination procedure. J. ACM 16, 349\u2013363 (1969)","journal-title":"J. ACM"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in prolog. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. LNCS, vol. 310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"key":"1_CR38","unstructured":"McCune, W.W.: Otter 3.0 reference manual and guide. Technical report, ANL-94\/6, Argonne National Laboratory, Argonne, IL (1994)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Musser, D.: On proving inductive properties of abstract data types. In: Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pp. 154\u2013162. ACM Press (1980)","DOI":"10.1145\/567446.567461"},{"key":"1_CR40","unstructured":"O\u2019Connor, J.J., Robertson, E.F.: Jacques Herbrand. http:\/\/www-history.mcs.st-andrews.ac.uk\/Biographies\/Herbrand.html. Accessed March 2015"},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-71070-7_23","volume-title":"Automated Reasoning","author":"J Otten","year":"2008","unstructured":"Otten, J.: PleanCoP 2.0 and ileanCoP 1.2: high performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 283\u2013291. Springer, Heidelberg (2008)"},{"issue":"2","key":"1_CR42","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1023\/A:1005847700447","volume":"18","author":"M Paramasivam","year":"1997","unstructured":"Paramasivam, M., Plaisted, D.: A replacement rule theorem prover. J. Autom. Reasoning 18(2), 221\u2013226 (1997)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR43","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"FJ Pelletier","year":"1986","unstructured":"Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reasoning 2, 191\u2013216 (1986)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR44","unstructured":"Plaisted, D.: A recursively defined ordering for proving termination of term rewriting systems. Technical report, R-78-943, University of Illinois at Urbana-Champaign, Urbana, IL (1978)"},{"key":"1_CR45","unstructured":"Plaisted, D.: Well-founded orderings for proving termination of systems of rewrite rules. Technical report, R-78-932, University of Illinois at Urbana-Champaign, Urbana, IL (1978)"},{"key":"1_CR46","unstructured":"Plaisted, D.: An efficient relevance criterion for mechanical theorem proving. In: Proceedings of the 1st Annual National Conference on Artificial Intelligence, pp. 79\u201383. AAAI Press (1980)"},{"issue":"2","key":"1_CR47","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","volume":"18","author":"D Plaisted","year":"1982","unstructured":"Plaisted, D.: A simplified problem reduction format. Artif. Intell. 18(2), 227\u2013261 (1982)","journal-title":"Artif. Intell."},{"key":"1_CR48","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"1_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-93862-6","volume-title":"The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis","author":"D Plaisted","year":"1997","unstructured":"Plaisted, D., Zhu, Y.: The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis. Vieweg, Wiesbaden (1997)"},{"issue":"1\u20132","key":"1_CR50","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0004-3702(02)00368-5","volume":"144","author":"D Plaisted","year":"2003","unstructured":"Plaisted, D., Yahya, A.: A relevance restriction strategy for automated deduction. Artif. Intell. 144(1\u20132), 59\u201393 (2003)","journal-title":"Artif. Intell."},{"issue":"3","key":"1_CR51","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"DA Plaisted","year":"1988","unstructured":"Plaisted, D.A.: Non-Horn clause logic programming without contrapositives. J. Autom. Reasoning 4(3), 287\u2013325 (1988)","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"1_CR52","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"DA Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reasoning 25(3), 167\u2013217 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR53","series-title":"Applied Logic Series","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-94-017-0437-3_9","volume-title":"Automated Deduction - A Basis for Applications","author":"W Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G.: Theorem proving in large theories. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications. Applied Logic Series, vol. 10, pp. 225\u2013241. Springer, Heidelberg (1998)"},{"key":"1_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-48660-7_26","volume-title":"Automated Deduction - CADE-16","author":"A Riazanov","year":"1999","unstructured":"Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 292\u2013296. Springer, Heidelberg (1999)"},{"volume-title":"Handbook of Automated Reasoning","year":"2001","key":"1_CR55","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"1_CR56","first-page":"227","volume":"1","author":"J Robinson","year":"1965","unstructured":"Robinson, J.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1(3), 227\u2013234 (1965)","journal-title":"Int. J. Comput. Math."},{"issue":"1","key":"1_CR57","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J Robinson","year":"1965","unstructured":"Robinson, J.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"1_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"key":"1_CR59","series-title":"Symbolic Computation","volume-title":"Automation of Reasoning 1: Classical Papers on Computational Logic 1957\u20131966","year":"1983","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning 1: Classical Papers on Computational Logic 1957\u20131966. Symbolic Computation. Springer, Heidelberg (1983)"},{"key":"1_CR60","series-title":"Symbolic Computation","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970","year":"1983","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970. Symbolic Computation. Springer, Heidelberg (1983)"},{"key":"1_CR61","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-45744-5_30","volume-title":"Automated Reasoning","author":"R Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: DCTP - a disconnection calculus theorem prover - system abstract. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 381\u2013385. Springer, Heidelberg (2001)"},{"issue":"3","key":"1_CR62","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M Stickel","year":"1981","unstructured":"Stickel, M.: A unification algorithm for associative-commutative functions. J. ACM 28(3), 423\u2013434 (1981)","journal-title":"J. ACM"},{"issue":"4","key":"1_CR63","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M Stickel","year":"1988","unstructured":"Stickel, M.: A prolog technology theorem prover: implementation by an extended prolog compiler. J. Autom. Reasoning 4(4), 353\u2013380 (1988)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"1_CR64","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure - the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS - a semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295\u2013310. Springer, Heidelberg (2007)"},{"key":"1_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009)"},{"key":"1_CR67","unstructured":"Wikipedia: Hilbert\u2019s program \u2013 Wikipedia, the free encyclopedia (2014). http:\/\/en.wikipedia.org\/wiki\/Hilbert\u2019sprogram. Accessed March 2015"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Wos, L., Carson, D., Robinson, G.: The unit preference strategy in theorem proving. In: Proceedings of the Fall Joint Computer Conference, Part I. AFIPS Conference Proceedings, vol. 26, pp. 615\u2013621 (1964)","DOI":"10.1145\/1464052.1464109"},{"key":"1_CR69","unstructured":"Zak, R.: Hilbert\u2019s program. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2015 edn. (2015). Accessed March 2015"},{"key":"1_CR70","unstructured":"Zalta, E.N.: Gottlob Frege. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy. Fall 2014 edn. (2014). Accessed March 2015"},{"key":"1_CR71","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0168-0072(89)90053-5","volume":"42","author":"N Zamov","year":"1989","unstructured":"Zamov, N.: Maslov\u2019s inverse method and decidable classes. Ann. Pure Appl. Logic 42, 165\u2013194 (1989)","journal-title":"Ann. Pure Appl. Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T17:12:26Z","timestamp":1748538746000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}