{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:22:16Z","timestamp":1758979336257,"version":"3.37.3"},"reference-count":84,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T00:00:00Z","timestamp":1730160000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T00:00:00Z","timestamp":1730160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004238","name":"Universit\u00e4t Potsdam","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004238","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to \u0141ukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of \u0141ukasiewicz \u2019s problem was automatically discovered that is much shorter than any proof found before by man or machine.<\/jats:p>","DOI":"10.1007\/s10817-024-09711-8","type":"journal-article","created":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T13:27:37Z","timestamp":1730294857000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Investigations into Proof Structures"],"prefix":"10.1007","volume":"68","author":[{"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]},{"given":"Wolfgang","family":"Bibel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,29]]},"reference":[{"key":"9711_CR1","volume-title":"Compilers\u2014Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers\u2014Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"9711_CR2","doi-asserted-by":"publisher","unstructured":"Astrachan, O.L., Stickel, M.E.: Caching and lemmaizing in model elimination theorem provers. In: Kapur, D. (ed.) CADE-11, pp. 224\u2013238. Springer, Berlin (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_168","DOI":"10.1007\/3-540-55602-8_168"},{"key":"9711_CR3","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) JELIA\u201996. LNCS (LNAI), vol. 1126, pp. 1\u201317. Springer, Berlin (1996).https:\/\/doi.org\/10.1007\/3-540-61630-6_1","DOI":"10.1007\/3-540-61630-6_1"},{"key":"9711_CR4","doi-asserted-by":"publisher","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg, Braunschweig (1982).https:\/\/doi.org\/10.1007\/978-3-322-90102-6. Second edition 1987","DOI":"10.1007\/978-3-322-90102-6"},{"key":"9711_CR5","volume-title":"Deduction: Automated Logic","author":"W Bibel","year":"1993","unstructured":"Bibel, W.: Deduction: Automated Logic. Academic Press, London (1993)"},{"key":"9711_CR6","unstructured":"Bibel, W.: Comparison of proof methods. In: Otten, J., Bibel, W. (eds.) AReCCa 2023. CEUR Workshop Proc., vol. 3613, pp. 119\u2013132. CEUR-WS.org, Aachen (2024)"},{"key":"9711_CR7","doi-asserted-by":"publisher","unstructured":"Bibel, W.: A conjecture for ATP research. CoRR abs\/2403.10334 (2024). https:\/\/doi.org\/10.48550\/2403.10334","DOI":"10.48550\/2403.10334"},{"key":"9711_CR8","doi-asserted-by":"publisher","unstructured":"Bibel, W., Otten, J.: From Sch\u00fctte\u2019s formal systems to modern automated deduction. In: Kahle, R., Rathjen, M. (eds.) The Legacy of Kurt Sch\u00fctte, pp. 215\u2013249. Springer, Cham (2020). Chap. 13. https:\/\/doi.org\/10.1007\/978-3-030-49424-7_13","DOI":"10.1007\/978-3-030-49424-7_13"},{"key":"9711_CR9","unstructured":"Bull, R., Cubrinovska, A.: Interview with Robert Bull. Popper and prior in New Zealand. http:\/\/popper-prior.nz\/items\/show\/255. Accessed 9 Jul 2024 (2018)"},{"issue":"2","key":"9711_CR10","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/BF01048619","volume":"4","author":"MW Bunder","year":"1995","unstructured":"Bunder, M.W.: A simplified form of condensed detachment. J. Log. Lang. Inf. 4(2), 169\u2013173 (1995). https:\/\/doi.org\/10.1007\/BF01048619","journal-title":"J. Log. Lang. Inf."},{"key":"9711_CR11","doi-asserted-by":"publisher","unstructured":"Claessen, K., Smallbone, N.: Efficient encodings of first-order Horn formulas in equational logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 388\u2013404. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_26","DOI":"10.1007\/978-3-319-94205-6_26"},{"key":"9711_CR12","first-page":"162","volume":"43","author":"N Dershowitz","year":"1991","unstructured":"Dershowitz, N., Jouannaud, J.: Notations for rewriting. Bull. EATCS 43, 162\u2013174 (1991)","journal-title":"Bull. EATCS"},{"issue":"4","key":"9711_CR13","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. JACM 27(4), 758\u2013771 (1980). https:\/\/doi.org\/10.1145\/322217.322228","journal-title":"JACM"},{"issue":"1","key":"9711_CR14","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","volume":"1","author":"E Eder","year":"1985","unstructured":"Eder, E.: Properties of substitutions and unification. J. Symb. Comput. 1(1), 31\u201346 (1985). https:\/\/doi.org\/10.1016\/S0747-7171(85)80027-4","journal-title":"J. Symb. Comput."},{"key":"9711_CR15","doi-asserted-by":"publisher","unstructured":"Eder, E.: A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods. In: B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL\u00a0\u201988. LNCS, vol. 385, pp. 80\u201398. Springer, Berlin (1989). https:\/\/doi.org\/10.1007\/BFb0026296","DOI":"10.1007\/BFb0026296"},{"key":"9711_CR16","doi-asserted-by":"publisher","unstructured":"Eder, E.: Relative Complexities of First Order Calculi. Vieweg, Braunschweig (1992). https:\/\/doi.org\/10.1007\/978-3-322-84222-0","DOI":"10.1007\/978-3-322-84222-0"},{"issue":"2","key":"9711_CR17","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10817-020-09576-7","volume":"65","author":"M F\u00e4rber","year":"2021","unstructured":"F\u00e4rber, M., Kaliszyk, C., Urban, J.: Machine learning guidance for connection tableaux. J. Autom. Reason. 65(2), 287\u2013320 (2021). https:\/\/doi.org\/10.1007\/s10817-020-09576-7","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9711_CR18","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":"9711_CR19","doi-asserted-by":"publisher","unstructured":"Flajolet, P., Sipala, P., Steyaert, J.: Analytic variations on the common subexpression problem. In: ICALP90. LNCS, vol. 443, pp. 220\u2013234. Springer, Berlin (1990). https:\/\/doi.org\/10.1007\/BFb0032034","DOI":"10.1007\/BFb0032034"},{"key":"9711_CR20","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, San Francisco, CA (1999). http:\/\/ijcai.org\/Proceedings\/99-1\/Papers\/001.pdf"},{"key":"9711_CR21","doi-asserted-by":"publisher","unstructured":"Fuchs, D., Fuchs, M.: CODE: A powerful prover for problems of condensed detachment. In: McCune, W. (ed.) CADE-14, pp. 260\u2013263. Springer, Berlin (1997). https:\/\/doi.org\/10.1007\/3-540-63104-6_25","DOI":"10.1007\/3-540-63104-6_25"},{"key":"9711_CR22","doi-asserted-by":"publisher","first-page":"105177","DOI":"10.1016\/j.jcta.2019.105177","volume":"172","author":"A Genitrini","year":"2020","unstructured":"Genitrini, A., Gittenberger, B., Kauers, M., Wallner, M.: Asymptotic enumeration of compacted binary trees of bounded right height. J. Comb. Theory Ser. A 172, 105177 (2020). https:\/\/doi.org\/10.1016\/j.jcta.2019.105177","journal-title":"J. Comb. Theory Ser. A"},{"key":"9711_CR23","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, Chap. 3, vol. 1, pp. 101\u2013178. Elsevier, Amsterdam (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50005-9","DOI":"10.1016\/b978-044450813-3\/50005-9"},{"key":"9711_CR24","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":"9711_CR25","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. Symb. Log. 55(1), 90\u2013105 (1990). https:\/\/doi.org\/10.2307\/2274956","journal-title":"J. Symb. Log."},{"key":"9711_CR26","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Chvalovsk\u00fd, K., Ols\u00e1k, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA anonymous: symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 448\u2013463. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29","DOI":"10.1007\/978-3-030-51054-1_29"},{"key":"9711_CR27","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/BF01371632","volume":"42","author":"JA Kalman","year":"1983","unstructured":"Kalman, J.A.: Condensed detachment as a rule of inference. Stud. Log. 42, 443\u2013451 (1983). https:\/\/doi.org\/10.1007\/BF01371632","journal-title":"Stud. Log."},{"key":"9711_CR28","unstructured":"Knuth, D.E.: The Art of Computer Programming: Volume 1\/Fundamental Algorithms. Addison-Wesley, Reading, MA (1968)"},{"key":"9711_CR29","doi-asserted-by":"publisher","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, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9711_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":"9711_CR31","unstructured":"Letz, R.: Tableau and connection calculi. structure, complexity, implementation. Habilitationsschrift, TU M\u00fcnchen (1999). https:\/\/web.archive.org\/web\/20230604101128\/https:\/\/www2.tcs.ifi.lmu.de\/~letz\/habil.ps. Accessed 9 Jul 2024"},{"issue":"3","key":"9711_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)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9711_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":"9711_CR34","doi-asserted-by":"publisher","unstructured":"Lohrey, M.: Grammar-based tree compression. In: Potapov, I. (ed.) DLT 2015. LNCS, vol. 9168, pp. 46\u201357. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21500-6_3","DOI":"10.1007\/978-3-319-21500-6_3"},{"issue":"8","key":"9711_CR35","doi-asserted-by":"publisher","first-page":"1150","DOI":"10.1016\/j.is.2013.06.006","volume":"38","author":"M Lohrey","year":"2013","unstructured":"Lohrey, M., Maneth, S., Mennicke, R.: XML tree structure compression using RePair. Inf. Syst. 38(8), 1150\u20131167 (2013). https:\/\/doi.org\/10.1016\/j.is.2013.06.006","journal-title":"Inf. Syst."},{"key":"9711_CR36","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":"9711_CR37","unstructured":"\u0141ukasiewicz, J.: The shortest axiom of the implicational calculus of propositions. In: Proc. of the Royal Irish Academy, vol. 52, Sect.\u00a0A, No.\u00a03, pp. 25\u201333 (1948). http:\/\/www.jstor.org\/stable\/20488489"},{"key":"9711_CR38","unstructured":"\u0141ukasiewicz, J.: Elements of Mathematical Logic. Pergamon Press, Oxford,: English translation of the second edition (1958) of Elementy logiki matematycznej. PWM, Warszawa (1963)"},{"key":"9711_CR39","unstructured":"\u0141ukasiewicz, J.: Selected Works. North-Holland, Amsterdam (1970)"},{"key":"9711_CR40","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 [39], pp.\u00a0131\u2013152"},{"key":"9711_CR41","doi-asserted-by":"publisher","unstructured":"Lusk, E.L., McCune, W.W.: Experiments with ROO, a parallel automated deduction system. In: Fronh\u00f6fer, B., Wrightson, G. (eds.) Parallelization in Inference Systems. LNCS (LNAI), vol. 590, pp. 139\u2013162. Springer, Berlin (1992). https:\/\/doi.org\/10.1007\/3-540-55425-4_6","DOI":"10.1007\/3-540-55425-4_6"},{"key":"9711_CR42","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 9 Jul 2024","DOI":"10.2172\/822573"},{"key":"9711_CR43","unstructured":"McCune, W.: Prover9 and Mace4. http:\/\/www.cs.unm.edu\/~mccune\/prover9. Accessed 9 Jul 2024 (2005\u20132010)"},{"key":"9711_CR44","doi-asserted-by":"publisher","unstructured":"McCune, W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) CADE-11. LNCS (LNAI), vol. 607, pp. 209\u2013223. Springer, Berlin (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_167","DOI":"10.1007\/3-540-55602-8_167"},{"issue":"3","key":"9711_CR45","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1305\/ndjfl\/1040149359","volume":"36","author":"ND Megill","year":"1995","unstructured":"Megill, N.D.: A finitely axiomatized formalization of predicate calculus with equality. Notre Dame J. Formal Logic 36(3), 435\u2013453 (1995). https:\/\/doi.org\/10.1305\/ndjfl\/1040149359","journal-title":"Notre Dame J. Formal Logic"},{"key":"9711_CR46","unstructured":"Megill, N., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs, 2nd edn. lulu.com (2019). https:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"issue":"4","key":"9711_CR47","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"},{"issue":"3","key":"9711_CR48","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":"9711_CR49","unstructured":"OEIS Foundation Inc.: The on-line encyclopedia of integer sequences (2022). http:\/\/oeis.org"},{"issue":"2\u20133","key":"9711_CR50","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."},{"key":"9711_CR51","doi-asserted-by":"publisher","unstructured":"Pfenning, F.: Single axioms in the implicational propositional calculus. In: Lusk, E., Overbeek, R. (eds.) CADE-9. LNCS (LNAI), vol. 310, pp. 710\u2013713. Springer, Berlin (1988). https:\/\/doi.org\/10.1007\/BFb0012869","DOI":"10.1007\/BFb0012869"},{"issue":"3","key":"9711_CR52","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":"9711_CR53","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":"9711_CR54","doi-asserted-by":"publisher","unstructured":"Rawson, M., Wernhard, C., Zombori, Z., Bibel, W.: Lemmas: Generation, selection, application. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS (LNAI), vol. 14278, pp. 153\u2013174. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_9. Extended version: https:\/\/arxiv.org\/abs\/2303.05854","DOI":"10.1007\/978-3-031-43513-3_9"},{"key":"9711_CR55","first-page":"63","volume":"2","author":"A Rezus","year":"1982","unstructured":"Rezus, A.: On a theorem of Tarski. Lib. Math. 2, 63\u201397 (1982)","journal-title":"Lib. Math."},{"key":"9711_CR56","unstructured":"Rezu\u015f, A.: Tarski singleton bases: 1925-1932 (on an allegedly lost \u2018method of proof\u2019 of Alfred Tarski) (2019). In: Witness Theory\u2014Notes on $$\\lambda $$-calculus and Logic. Studies in Logic, vol. 84, pp. 227\u2013243. College Publications, London (2020). Preprint (2019). https:\/\/doi.org\/10.13140\/RG.2.2.10955.34081"},{"key":"9711_CR57","unstructured":"Rezu\u015f, A.: Tarski\u2019s Claim thirty years later (2010). In: Witness Theory\u2014Notes on $$\\lambda $$-Calculus and Logic. Studies in Logic, vol. 84, pp. 217\u2013225. College Publications, London (2020). Preprint (2016). http:\/\/www.equivalences.org\/editions\/proof-theory\/ar-tc-20160512.pdf"},{"key":"9711_CR58","unstructured":"Rezu\u015f, A.: Witness Theory\u2014Notes on $$\\lambda $$-Calculus and Logic. Studies in Logic, vol. 84. College Publications, London (2020)"},{"issue":"1","key":"9711_CR59","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM 12(1), 23\u201341 (1965)","journal-title":"JACM"},{"key":"9711_CR60","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE\u00a027. LNAI, pp. 495\u2013507. Springer, Cham (2019).https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"9711_CR61","doi-asserted-by":"publisher","unstructured":"Schumann, J.M.P.: DELTA\u2014a bottom-up preprocessor for top-down theorem provers. In: CADE-12. LNCS (LNAI), vol. 814, pp. 774\u2013777. Springer, Berlin (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_58","DOI":"10.1007\/3-540-58156-1_58"},{"key":"9711_CR62","unstructured":"Soboc\u00ednski, B.: Z bada\u0144 nad teori\u0105 dedukcji. Przegl\u0105d Filozoficzny 35, 171\u2013193 (1932). Excerpts translated into English and edited by A. Rezu\u015f are published as [58, p. 257-268 (Appendix: Boles\u0142aw Soboc\u00ednski 1932, \u00a71)]"},{"issue":"4","key":"9711_CR63","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."},{"key":"9711_CR64","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"key":"9711_CR65","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. AI 131(1\u20132), 39\u201354 (2001). https:\/\/doi.org\/10.1016\/S0004-3702(01)00113-8","DOI":"10.1016\/S0004-3702(01)00113-8"},{"issue":"1","key":"9711_CR66","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1305\/ndjfl\/1093893855","volume":"11","author":"I Thomas","year":"1970","unstructured":"Thomas, I.: Final word on a shortest implicational axiom. Notre Dame J. Formal Logic 11(1), 16 (1970)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"9711_CR67","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":"9711_CR68","unstructured":"Ulrich, D.: Sentential Calculi Pages. https:\/\/web.ics.purdue.edu\/~dulrich\/Home-page.htm. Accessed 9 Jul 2024 (2007)"},{"key":"9711_CR69","doi-asserted-by":"publisher","unstructured":"Ulrich, D.: Single axioms and axiom-pairs for the implicational fragments of R, R-Mingle, and some related systems. In: Bimb\u00f3, K. (ed.) J.\u00a0Michael Dunn on Information Based Logics. Outstanding Contributions to Logic, vol. 8, pp. 53\u201380. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29300-4_4","DOI":"10.1007\/978-3-319-29300-4_4"},{"issue":"3","key":"9711_CR70","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996). https:\/\/doi.org\/10.1007\/BF00252178","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9711_CR71","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":"9711_CR72","unstructured":"Veroff, R.: Challenge problems with condensed detachment (2011). https:\/\/www.cs.unm.edu\/~veroff\/CD\/. Accessed 9 Jul 2024"},{"key":"9711_CR73","unstructured":"Walsh, M., Fitelson, B.: Answers to some open questions of Ulrich and Meredith (2021). Under review. http:\/\/fitelson.org\/walsh.pdf. Accessed 9 Jul 2024"},{"key":"9711_CR74","doi-asserted-by":"publisher","unstructured":"Wernhard, C.: CD Tools\u2014condensed detachment and structure generating theorem proving (system description). CoRR abs\/2207.08453 (2022). https:\/\/doi.org\/10.48550\/arXiv.2207.08453","DOI":"10.48550\/arXiv.2207.08453"},{"key":"9711_CR75","unstructured":"Wernhard, C.: Generating compressed combinatory proof structures\u2014an approach to automated first-order theorem proving. In: Konev, B., Schon, C., Steen, A. (eds.) PAAR\u00a02022. CEUR Workshop Proc., vol. 3201. CEUR-WS.org, Aachen (2022). https:\/\/arxiv.org\/abs\/2209.12592"},{"key":"9711_CR76","unstructured":"Wernhard, C.: Structure-generating first-order theorem proving. In: Otten, J., Bibel, W. (eds.) AReCCa 2023. CEUR Workshop Proc., vol. 3613, pp. 64\u201383. CEUR-WS.org, Aachen (2024). https:\/\/ceur-ws.org\/Vol-3613\/AReCCa2023_paper5.pdf"},{"key":"9711_CR77","doi-asserted-by":"publisher","unstructured":"Wernhard, C., Bibel, W.: Learning from \u0141ukasiewicz and Meredith: investigations into proof structures. In: Platzer, A., Sutcliffe, G. (eds.) CADE\u00a028. LNCS (LNAI), vol. 12699, pp. 58\u201375. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_4","DOI":"10.1007\/978-3-030-79876-5_4"},{"key":"9711_CR78","doi-asserted-by":"publisher","unstructured":"Wernhard, C., Bibel, W.: Learning from \u0141ukasiewicz and Meredith: investigations into proof structures (extended version). CoRR abs\/2104.13645 (2021). https:\/\/doi.org\/10.48550\/arXiv.2104.13645","DOI":"10.48550\/arXiv.2104.13645"},{"issue":"1\u20132","key":"9711_CR79","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":"9711_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. Automated Reasoning Series, pp. 297\u2013345. Kluwer Academic Publishers, Dordrecht (1991). https:\/\/doi.org\/10.1007\/978-94-011-3488-0_15","DOI":"10.1007\/978-94-011-3488-0_15"},{"issue":"2","key":"9711_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":"9711_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."},{"issue":"2","key":"9711_CR83","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":"9711_CR84","doi-asserted-by":"publisher","unstructured":"Wos, L., Winker, S., McCune, W., Overbeek, R., Lusk, E., Stevens, R., Butler, R.: Automated reasoning contributes to mathematics and logic. In: Stickel, M.E. (ed.) CADE-10, pp. 485\u2013499. Springer, Berlin (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_109","DOI":"10.1007\/3-540-52885-7_109"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09711-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09711-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09711-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,14]],"date-time":"2024-12-14T07:07:52Z","timestamp":1734160072000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09711-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,29]]},"references-count":84,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["9711"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09711-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,10,29]]},"assertion":[{"value":"16 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 October 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"24"}}