{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:46:32Z","timestamp":1743129992334,"version":"3.40.3"},"publisher-location":"Cham","reference-count":85,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031435126"},{"type":"electronic","value":"9783031435133"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T00:00:00Z","timestamp":1694649600000},"content-version":"vor","delay-in-days":256,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.<\/jats:p>","DOI":"10.1007\/978-3-031-43513-3_9","type":"book-chapter","created":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:02:36Z","timestamp":1694613756000},"page":"153-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Lemmas: Generation, Selection, Application"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0438-8829","authenticated-orcid":false,"given":"Christoph","family":"Wernhard","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8622-5304","authenticated-orcid":false,"given":"Zsolt","family":"Zombori","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3892-0171","authenticated-orcid":false,"given":"Wolfgang","family":"Bibel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"key":"9_CR1","unstructured":"Alemi, A.A., Chollet, F., Een, N., Irving, G., Szegedy, C., Urban, J.: DeepMath \u2013 deep sequence models for premise selection. In: Lee, D., et al. (eds.) NIPS 2016, pp. 2243\u20132251. Curran Associates Inc., USA (2016). http:\/\/dl.acm.org\/citation.cfm?id=3157096.3157347"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/3-540-55602-8_168","volume-title":"Automated Deduction\u2014CADE-11","author":"OL Astrachan","year":"1992","unstructured":"Astrachan, O.L., Stickel, M.E.: Caching and lemmaizing in model elimination theorem provers. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 224\u2013238. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_168"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 2, pp. 19\u201399. Elsevier (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50004-7","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61630-6_1","volume-title":"Logics in Artificial Intelligence","author":"P Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1\u201317. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61630-6_1"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C., Fuenmayor, D., Steen, A., Sutcliffe, G.: Who finds the short proof? Logic J. IGPL (2023). https:\/\/doi.org\/10.1093\/jigpal\/jzac082","DOI":"10.1093\/jigpal\/jzac082"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg, Braunschweig (1987). First edition 1982. https:\/\/doi.org\/10.1007\/978-3-322-90102-6","DOI":"10.1007\/978-3-322-90102-6"},{"key":"9_CR7","volume-title":"Deduction: Automated Logic","author":"W Bibel","year":"1993","unstructured":"Bibel, W.: Deduction: Automated Logic. Academic Press, Cambridge (1993)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-49424-7_13","volume-title":"The Legacy of Kurt Sch\u00fctte","author":"W Bibel","year":"2020","unstructured":"Bibel, W., Otten, J.: From Sch\u00fctte\u2019s formal systems to modern automated deduction. In: The Legacy of Kurt Sch\u00fctte, pp. 217\u2013251. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-49424-7_13"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/3-540-48317-9_3","volume-title":"Artificial Intelligence Today","author":"MP Bonacina","year":"1999","unstructured":"Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M.J., Veloso, M. (eds.) Artificial Intelligence Today. LNCS (LNAI), vol. 1600, pp. 43\u201384. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48317-9_3"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00250612","volume":"16","author":"G Boolos","year":"1987","unstructured":"Boolos, G.: A curious inference. J. Philos. Logic 16, 1\u201312 (1987). https:\/\/doi.org\/10.1007\/BF00250612","journal-title":"J. Philos. Logic"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","volume":"53","author":"JP Bridge","year":"2014","unstructured":"Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving. J. Autom. Reason. 53(2), 141\u2013172 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9301-5","journal-title":"J. Autom. Reason."},{"key":"9_CR12","unstructured":"Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the Mizar mathematical library. In: Bonacina, M.P., Furbach, U. (eds.) FTP 1997, pp. 58\u201362. RISC-Linz Report Series No. 97-50, Joh. Kepler Univ. Linz (1997). https:\/\/www.logic.at\/ftp97\/papers\/dahn.pdf"},{"issue":"2","key":"9_CR13","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT \u2013 a distributed and learning equational prover. J. Autom. Reason. 18(2), 189\u2013198 (1997). https:\/\/doi.org\/10.1023\/A:1005879229581","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s10817-018-9462-8","volume":"63","author":"G Ebner","year":"2018","unstructured":"Ebner, G., Hetzl, S., Leitsch, A., Reis, G., Weller, D.: On the generation of quantified lemmas. J. Autom. Reason. 63(1), 95\u2013126 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9462-8","journal-title":"J. Autom. Reason."},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BFb0026296","volume-title":"CSL \u201988","author":"E Eder","year":"1989","unstructured":"Eder, E.: A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods. In: B\u00f6rger, E., B\u00fcning, H.K., Richter, M.M. (eds.) CSL 1988. LNCS, vol. 385, pp. 80\u201398. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0026296"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1023\/A:1010695827789","volume":"27","author":"B Fitelson","year":"2001","unstructured":"Fitelson, B., Wos, L.: Missing proofs found. J. Autom. Reason. 27(2), 201\u2013225 (2001). https:\/\/doi.org\/10.1023\/A:1010695827789","journal-title":"J. Autom. Reason."},{"key":"9_CR17","unstructured":"Fuchs, M.: Lemma generation for model elimination by combining top-down and bottom-up inference. In: Dean, T. (ed.) IJCAI 1999, pp. 4\u20139. Morgan Kaufmann (1999). http:\/\/ijcai.org\/Proceedings\/99-1\/Papers\/001.pdf"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: Learning to prove with tactics. CoRR abs\/1804.00596 (2018). https:\/\/doi.org\/10.48550\/arXiv.1804.00596","DOI":"10.48550\/arXiv.1804.00596"},{"key":"9_CR19","unstructured":"Hester, J.: Novel methods for first order automated theorem proving. Ph.D. thesis, University of Florida (2021)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-28717-6_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Hetzl","year":"2012","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 228\u2013242. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_19"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 3, pp. 101\u2013178. Elsevier (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50005-9","DOI":"10.1016\/b978-044450813-3\/50005-9"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Hindley, J.R.: Basic Simple Type Theory. Cambridge University Press, Cambridge (1997). https:\/\/doi.org\/10.1017\/CBO9780511608865","DOI":"10.1017\/CBO9780511608865"},{"issue":"1","key":"9_CR23","doi-asserted-by":"publisher","first-page":"90","DOI":"10.2307\/2274956","volume":"55","author":"JR Hindley","year":"1990","unstructured":"Hindley, J.R., Meredith, D.: Principal type-schemes and condensed detachment. J. Symbolic Logic 55(1), 90\u2013105 (1990). https:\/\/doi.org\/10.2307\/2274956","journal-title":"J. Symbolic Logic"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Holden, S.B.: Machine learning for automated theorem proving: learning to solve SAT and QSAT. Found. Trends\u00ae Mach. Learn. 14(6), 807\u2013989 (2021). https:\/\/doi.org\/10.1561\/2200000081","DOI":"10.1561\/2200000081"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-62075-6_20","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2017","unstructured":"Jakub\u016fv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292\u2013302. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109\u2013128 (2015). https:\/\/doi.org\/10.1016\/j.jsc.2014.09.032","journal-title":"J. Symb. Comput."},{"key":"9_CR27","unstructured":"Kaliszyk, C., Urban, J., Michalewski, H., Ols\u00e1k, M.: Reinforcement learning of theorem proving. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) NeurIPS 2018, pp. 8836\u20138847 (2018). https:\/\/papers.nips.cc\/paper\/2018\/file\/55acf8539596d25624059980986aaa78-Paper.pdf"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-24246-0_21","volume-title":"Frontiers of Combining Systems","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Lemmatization for stronger reasoning in large theories. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 341\u2013356. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_21"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Lemmon, E.J., Meredith, C.A., Meredith, D., Prior, A.N., Thomas, I.: Calculi of pure strict implication. In: Davis, J.W., Hockney, D.J., Wilson, W.K. (eds.) Philosophical Logic, pp. 215\u2013250. Springer, Dordrecht (1969). https:\/\/doi.org\/10.1007\/978-94-010-9614-0_17. Reprint of a technical report, Canterbury University College, Christchurch (1957)","DOI":"10.1007\/978-94-010-9614-0_17"},{"key":"9_CR31","unstructured":"Letz, R.: Tableau and Connection Calculi. Structure, Complexity, Implementation. Habilitationsschrift, TU M\u00fcnchen (1999). http:\/\/www2.tcs.ifi.lmu.de\/~letz\/habil.ps. Accessed 19 July 2023"},{"issue":"3","key":"9_CR32","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R Letz","year":"1994","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection tableaux calculi. J. Autom. Reason. 13(3), 297\u2013337 (1994). https:\/\/doi.org\/10.1007\/BF00881947","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9_CR33","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reason. 8(2), 183\u2013212 (1992). https:\/\/doi.org\/10.1007\/BF00244282","journal-title":"J. Autom. Reason."},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21. EPiC, vol. 56, pp. 85\u2013105 (2017). https:\/\/doi.org\/10.29007\/8mwc","DOI":"10.29007\/8mwc"},{"key":"9_CR35","volume-title":"Automated Theorem Proving: A Logical Basis","author":"DW Loveland","year":"1978","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam (1978)"},{"key":"9_CR36","unstructured":"\u0141ukasiewicz, J.: Selected Works. North Holland (1970). Edited by L. Borkowski"},{"key":"9_CR37","unstructured":"\u0141ukasiewicz, J., Tarski, A.: Untersuchungen \u00fcber den Aussagenkalk\u00fcl. Comptes rendus des s\u00e9ances de la Soc. d. Sciences et d. Lettres de Varsovie 23 (1930). English translation in [36], pp. 131\u2013152"},{"key":"9_CR38","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.3 reference manual. Technical report, ANL\/MCS-TM-263, Argonne National Laboratory (2003). https:\/\/www.cs.unm.edu\/~mccune\/otter\/Otter33.pdf. Accessed 19 July 2023","DOI":"10.2172\/822573"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-55602-8_167","volume-title":"Automated Deduction\u2014CADE-11","author":"W McCune","year":"1992","unstructured":"McCune, W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 209\u2013223. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_167"},{"issue":"3","key":"9_CR41","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1305\/ndjfl\/1093957574","volume":"4","author":"CA Meredith","year":"1963","unstructured":"Meredith, C.A., Prior, A.N.: Notes on the axiomatics of the propositional calculus. Notre Dame J. Formal Logic 4(3), 171\u2013187 (1963). https:\/\/doi.org\/10.1305\/ndjfl\/1093957574","journal-title":"Notre Dame J. Formal Logic"},{"key":"9_CR42","first-page":"155","volume":"1","author":"CA Meredith","year":"1953","unstructured":"Meredith, C.A.: Single axioms for the systems (C, N), (C, O) and (A, N) of the two-valued propositional calculus. J. Comput. Syst. 1, 155\u2013164 (1953)","journal-title":"J. Comput. Syst."},{"issue":"4","key":"9_CR43","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1305\/ndjfl\/1093888116","volume":"18","author":"D Meredith","year":"1977","unstructured":"Meredith, D.: In memoriam: Carew Arthur Meredith (1904\u20131976). Notre Dame J. Formal Logic 18(4), 513\u2013516 (1977). https:\/\/doi.org\/10.1305\/ndjfl\/1093888116","journal-title":"Notre Dame J. Formal Logic"},{"key":"9_CR44","unstructured":"OEIS Foundation Inc.: The On-Line Encyclopedia of Integer Sequences (2021). http:\/\/oeis.org"},{"issue":"2\u20133","key":"9_CR45","doi-asserted-by":"publisher","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2\u20133), 159\u2013182 (2010). https:\/\/doi.org\/10.3233\/AIC-2010-0464","journal-title":"AI Commun."},{"issue":"1\u20132","key":"9_CR46","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1\u20132), 139\u2013161 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00037-3","journal-title":"J. Symb. Comput."},{"key":"9_CR47","unstructured":"Paszke, A., et al.: PyTorch: an imperative style, high-performance deep learning library. In: Advances in Neural Information Processing Systems, vol. 32, pp. 8024\u20138035. Curran Associates, Inc. (2019). http:\/\/papers.neurips.cc\/paper\/9015-pytorch-an-imperative-style-high-performance-deep-learning-library.pdf"},{"key":"9_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-030-53518-6_23","volume-title":"Intelligent Computer Mathematics","author":"B Piotrowski","year":"2020","unstructured":"Piotrowski, B., Urban, J.: Guiding inferences in connection tableau by recurrent neural networks. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 309\u2013314. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_23"},{"key":"9_CR49","doi-asserted-by":"publisher","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. CoRR abs\/2009.03393 (2020). https:\/\/doi.org\/10.48550\/arXiv.2009.03393","DOI":"10.48550\/arXiv.2009.03393"},{"issue":"3","key":"9_CR50","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1080\/00048405685200181","volume":"34","author":"AN Prior","year":"1956","unstructured":"Prior, A.N.: Logicians at play; or Syll, Simp and Hilbert. Australas. J. Philos. 34(3), 182\u2013192 (1956). https:\/\/doi.org\/10.1080\/00048405685200181","journal-title":"Australas. J. Philos."},{"key":"9_CR51","doi-asserted-by":"publisher","unstructured":"Prior, A.N.: Formal Logic, 2nd edn. Clarendon Press, Oxford (1962). https:\/\/doi.org\/10.1093\/acprof:oso\/9780198241560.001.0001","DOI":"10.1093\/acprof:oso\/9780198241560.001.0001"},{"key":"9_CR52","unstructured":"Pudl\u00e1k, P.: Search for faster and shorter proofs using machine generated lemmas. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR Workshop Proceeding, vol. 192, pp. 34\u201353. CEUR-WS.org (2006). http:\/\/ceur-ws.org\/Vol-192\/paper03.pdf"},{"key":"9_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-86059-2_11","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Rawson","year":"2021","unstructured":"Rawson, M., Reger, G.: lazyCoP: lazy paramodulation meets neurally guided search. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 187\u2013199. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_11"},{"key":"9_CR54","doi-asserted-by":"publisher","unstructured":"Rawson, M., Wernhard, C., Zombori, Z., Bibel, W.: Lemmas: generation, selection, application. CoRR abs\/2303.05854 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.05854","DOI":"10.48550\/arXiv.2303.05854"},{"key":"9_CR55","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-319-21401-6_23","volume-title":"Automated Deduction - CADE-25","author":"G Reger","year":"2015","unstructured":"Reger, G., Tishkovsky, D., Voronkov, A.: Cooperating proof attempts. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 339\u2013355. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_23"},{"key":"9_CR56","unstructured":"Rezu\u015f, A.: Tarski\u2019s Claim thirty years later. In: Witness Theory - Notes on $$\\lambda $$-calculus and Logic, Studies in Logic, vol. 84, pp. 217\u2013225. College Publications (2020). Preprint (2016). http:\/\/www.equivalences.org\/editions\/proof-theory\/ar-tc-20160512.pdf"},{"key":"9_CR57","unstructured":"Rezu\u015f, A.: Witness Theory - Notes on $$\\lambda $$-calculus and Logic. Studies in Logic, vol. 84. College Publications (2020)"},{"key":"9_CR58","doi-asserted-by":"publisher","unstructured":"Sanchez-Lengeling, B., Reif, E., Pearce, A., Wiltschko, A.B.: A gentle introduction to graph neural networks. Distill (2021). https:\/\/doi.org\/10.23915\/distill.00033","DOI":"10.23915\/distill.00033"},{"key":"9_CR59","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"key":"9_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"774","DOI":"10.1007\/3-540-58156-1_58","volume-title":"Automated Deduction \u2014 CADE-12","author":"JMP Schumann","year":"1994","unstructured":"Schumann, J.M.P.: DELTA \u2014 a bottom-up preprocessor for top-down theorem provers. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 774\u2013777. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_58"},{"issue":"4","key":"9_CR61","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"ME Stickel","year":"1988","unstructured":"Stickel, M.E.: A Prolog technology theorem prover: implementation by an extended Prolog compiler. J. Autom. Reason. 4(4), 353\u2013380 (1988). https:\/\/doi.org\/10.1007\/BF00297245","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9_CR62","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF00881955","volume":"13","author":"ME Stickel","year":"1994","unstructured":"Stickel, M.E.: Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction. J. Autom. Reason. 13(2), 189\u2013210 (1994). https:\/\/doi.org\/10.1007\/BF00881955","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9_CR63","first-page":"99","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition \u2013 CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"issue":"4","key":"9_CR64","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reason."},{"key":"9_CR65","unstructured":"Sutcliffe, G., Gao, Y., Colton, S.: A grand challenge of theorem discovery. In: Worksh. Challenges and Novel Applications for Automated Reasoning, 19th IJCAR, pp. 1\u201311 (2003). https:\/\/www.cs.miami.edu\/home\/geoff\/Papers\/Conference\/2003_SGC03_CNAAR-1-11.pdf"},{"issue":"2","key":"9_CR66","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1010683508225","volume":"27","author":"D Ulrich","year":"2001","unstructured":"Ulrich, D.: A legacy recalled and a tradition continued. J. Autom. Reason. 27(2), 97\u2013122 (2001). https:\/\/doi.org\/10.1023\/A:1010683508225","journal-title":"J. Autom. Reason."},{"key":"9_CR67","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-53518-6_24","volume-title":"Intelligent Computer Mathematics","author":"J Urban","year":"2020","unstructured":"Urban, J., Jakub\u016fv, J.: First neural conjecturing datasets and experiments. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 315\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_24"},{"key":"9_CR68","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441\u2013456. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_37"},{"issue":"2","key":"9_CR69","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1023\/A:1010635625063","volume":"27","author":"R Veroff","year":"2001","unstructured":"Veroff, R.: Finding shortest proofs: an application of linked inference rules. J. Autom. Reason. 27(2), 123\u2013139 (2001). https:\/\/doi.org\/10.1023\/A:1010635625063","journal-title":"J. Autom. Reason."},{"key":"9_CR70","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Guyon, I., et al. (eds.) NIPS 2017, pp. 2783\u20132793 (2017). http:\/\/papers.nips.cc\/paper\/6871-premise-selection-for-theorem-proving-by-deep-graph-embedding"},{"key":"9_CR71","unstructured":"Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proceedings, vol. 1635, pp. 125\u2013138. CEUR-WS.org (2016). http:\/\/ceur-ws.org\/Vol-1635\/paper-11.pdf"},{"key":"9_CR72","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-46714-2_11","volume-title":"Declarative Programming and Knowledge Management","author":"C Wernhard","year":"2020","unstructured":"Wernhard, C.: Facets of the PIE environment for proving, interpolating and eliminating on the basis of first-order logic. In: Hofstedt, P., Abreu, S., John, U., Kuchen, H., Seipel, D. (eds.) INAP\/WLP\/WFLP -2019. LNCS (LNAI), vol. 12057, pp. 160\u2013177. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-46714-2_11"},{"key":"9_CR73","unstructured":"Wernhard, C.: Generating compressed combinatory proof structures \u2013 an approach to automated first-order theorem proving. In: Konev, B., Schon, C., Steen, A. (eds.) PAAR 2022. CEUR Workshop Proceedings, vol. 3201. CEUR-WS.org (2022). https:\/\/arxiv.org\/abs\/2209.12592"},{"key":"9_CR74","doi-asserted-by":"publisher","unstructured":"Wernhard, C.: CD Tools \u2013 Condensed detachment and structure generating theorem proving (system description). CoRR abs\/2207.08453 (2023). https:\/\/doi.org\/10.48550\/arXiv.2207.08453","DOI":"10.48550\/arXiv.2207.08453"},{"key":"9_CR75","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-79876-5_4","volume-title":"Automated Deduction \u2013 CADE 28","author":"C Wernhard","year":"2021","unstructured":"Wernhard, C., Bibel, W.: Learning from \u0141ukasiewicz and Meredith: investigations into proof structures. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 58\u201375. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_4"},{"key":"9_CR76","doi-asserted-by":"publisher","unstructured":"Wernhard, C., Bibel, W.: Investigations into proof structures. CoRR abs\/2304.12827 (2023, submitted). https:\/\/doi.org\/10.48550\/arXiv.2304.12827","DOI":"10.48550\/arXiv.2304.12827"},{"issue":"1\u20132","key":"9_CR77","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1017\/S1471068411000494","volume":"12","author":"J Wielemaker","year":"2012","unstructured":"Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-prolog. Theory Pract. Logic Program. 12(1\u20132), 67\u201396 (2012). https:\/\/doi.org\/10.1017\/S1471068411000494","journal-title":"Theory Pract. Logic Program."},{"key":"9_CR78","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-17511-4_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Woltzenlogel Paleo","year":"2010","unstructured":"Woltzenlogel Paleo, B.: Atomic cut introduction by resolution: proof structuring and compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 463\u2013480. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_26"},{"key":"9_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-52885-7_109","volume-title":"10th International Conference on Automated Deduction","author":"L Wos","year":"1990","unstructured":"Wos, L., et al.: Automated reasoning contributes to mathematics and logic. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 485\u2013499. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_109"},{"key":"9_CR80","doi-asserted-by":"publisher","unstructured":"Wos, L.: Automated reasoning and Bledsoe\u2019s dream for the field. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 297\u2013345. Automated Reasoning Series, Kluwer Academic Publishers (1991). https:\/\/doi.org\/10.1007\/978-94-011-3488-0_15","DOI":"10.1007\/978-94-011-3488-0_15"},{"issue":"2","key":"9_CR81","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0898-1221(94)00220-F","volume":"29","author":"L Wos","year":"1995","unstructured":"Wos, L.: The resonance strategy. Comput. Math. Appl. 29(2), 133\u2013178 (1995). https:\/\/doi.org\/10.1016\/0898-1221(94)00220-F","journal-title":"Comput. Math. Appl."},{"issue":"1","key":"9_CR82","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF00247668","volume":"17","author":"L Wos","year":"1996","unstructured":"Wos, L.: The power of combining resonance with heat. J. Autom. Reason. 17(1), 23\u201381 (1996). https:\/\/doi.org\/10.1007\/BF00247668","journal-title":"J. Autom. Reason."},{"key":"9_CR83","unstructured":"Wos, L.: Lemma inclusion versus lemma adjunction. Assoc. Autom. Reason. Newsl. 44 (1999). https:\/\/aarinc.org\/Newsletters\/044-1999-09.html. Accessed 19 July 2023"},{"issue":"2","key":"9_CR84","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1023\/A:1010691726881","volume":"27","author":"L Wos","year":"2001","unstructured":"Wos, L.: Conquering the Meredith single axiom. J. Autom. Reason. 27(2), 175\u2013199 (2001). https:\/\/doi.org\/10.1023\/A:1010691726881","journal-title":"J. Autom. Reason."},{"key":"9_CR85","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/978-3-030-51054-1_33","volume-title":"Automated Reasoning","author":"Z Zombori","year":"2020","unstructured":"Zombori, Z., Urban, J., Brown, C.E.: Prolog technology reinforcement\u00a0learning prover. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 489\u2013507. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_33"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43513-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:04:36Z","timestamp":1694613876000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43513-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031435126","9783031435133"],"references-count":85,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43513-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"14 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/tableaux2023.tableaux-ar.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 (2.92)","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}