{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:55:38Z","timestamp":1743080138851,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of \u201caxiom(s) and rule(s) imply goal(s)\u201d. The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by \u0141ukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_4","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"58-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Learning from \u0141ukasiewicz and Meredith: Investigations into Proof Structures"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0438-8829","authenticated-orcid":false,"given":"Christoph","family":"Wernhard","sequence":"first","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":[[2021,7,5]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","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-90100-2"},{"key":"4_CR2","unstructured":"Bibel, W.: Deduction: Automated Logic. Academic Press, London (1993)"},{"key":"4_CR3","doi-asserted-by":"crossref","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, chap. 13, pp. 215\u2013249. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-49424-7_13","DOI":"10.1007\/978-3-030-49424-7_13"},{"key":"4_CR4","doi-asserted-by":"crossref","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","DOI":"10.1007\/BF01048619"},{"key":"4_CR5","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\u201997. pp. 58\u201362. RISC-Linz Report Series No. 97\u201350, Joh. Kepler Univ., Linz (1997), https:\/\/www.logic.at\/ftp97\/papers\/dahn.pdf"},{"key":"4_CR6","unstructured":"Dershowitz, N., Jouannaud, J.: Notations for rewriting. Bull. EATCS 43, 162\u2013174 (1991)"},{"key":"4_CR7","doi-asserted-by":"crossref","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","DOI":"10.1145\/322217.322228"},{"key":"4_CR8","doi-asserted-by":"crossref","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"},{"key":"4_CR9","doi-asserted-by":"publisher","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","DOI":"10.1016\/S0747-7171(85)80027-4"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"F\u00e4rber, M., Kaliszyk, C., Urban, J.: Machine learning guidance for connection tableaux. J. Autom. Reasoning 65(2), 287\u2013320 (2021). https:\/\/doi.org\/10.1007\/s10817-020-09576-7","DOI":"10.1007\/s10817-020-09576-7"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Fitelson, B., Wos, L.: Missing proofs found. J. Autom. Reasoning 27(2), 201\u2013225 (2001). https:\/\/doi.org\/10.1023\/A:1010695827789","DOI":"10.1023\/A:1010695827789"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Leitsch, A., Reis, G., Weller, D.: Algorithmic introduction of quantified cuts. Theor. Comput. Sci. 549, 1\u201316 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.05.018","DOI":"10.1016\/j.tcs.2014.05.018"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Hindley, J.R., Meredith, D.: Principal type-schemes and condensed detachment. Journal of Symbolic Logic 55(1), 90\u2013105 (1990). https:\/\/doi.org\/10.2307\/2274956","DOI":"10.2307\/2274956"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. 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":"4_CR15","doi-asserted-by":"crossref","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, vol. 12167, pp. 448\u2013463. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29","DOI":"10.1007\/978-3-030-51054-1_29"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Kalman, J.A.: Condensed detachment as a rule of inference. Studia Logica 42, 443\u2013451 (1983). https:\/\/doi.org\/10.1007\/BF01371632","DOI":"10.1007\/BF01371632"},{"key":"4_CR17","doi-asserted-by":"crossref","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 Netherlands, 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":"4_CR18","doi-asserted-by":"publisher","unstructured":"Lohrey, M.: Grammar-based tree compression. In: Potapov, I. (ed.) DLT 2015. LNCS, vol.\u00a09168, pp. 46\u201357. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21500-6_3","DOI":"10.1007\/978-3-319-21500-6_3"},{"key":"4_CR19","unstructured":"\u0141ukasiewicz, J.: The shortest axiom of the implicational calculus of propositions. In: Proc. of the Royal Irish Academy. vol. 52, Sect. A, No. 3, pp. 25\u201333 (1948), http:\/\/www.jstor.org\/stable\/20488489, republished in [20], p. 295\u2013305"},{"key":"4_CR20","unstructured":"\u0141ukasiewicz, J.: Selected Works. North Holland (1970), edited by L. Borkowski"},{"key":"4_CR21","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 [20], p. 131\u2013152"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Lusk, Ewing L., McCune, William W.: Experiments with Roo, a parallel automated deduction system. In: Fronh\u00f6fer, B., Wrightson, G. (eds.) Parallelization in Inference Systems. LNCS, vol. 590, pp. 139\u2013162. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55425-4_6","DOI":"10.1007\/3-540-55425-4_6"},{"key":"4_CR23","doi-asserted-by":"publisher","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","DOI":"10.1007\/3-540-55602-8_167"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Meredith, C.A., Prior, A.N.: Notes on the axiomatics of the propositional calculus. Notre Dame J. of Formal Logic 4(3), 171\u2013187 (1963). https:\/\/doi.org\/10.1305\/ndjfl\/1093957574","DOI":"10.1305\/ndjfl\/1093957574"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Meredith, D.: In memoriam: Carew Arthur Meredith (1904\u20131976). Notre Dame J. of Formal Logic 18(4), 513\u2013516 (10 1977). https:\/\/doi.org\/10.1305\/ndjfl\/1093888116","DOI":"10.1305\/ndjfl\/1093888116"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Pelzer, B., Wernhard, C.: System description: E-KRHyper. In: Pfenning, F. (ed.) CADE-21. LNCS (LNAI), vol. 4603, pp. 503\u2013513. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_37","DOI":"10.1007\/978-3-540-73595-3_37"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Pfenning, Frank: Single axioms in the implicational propositional calculus. In: Lusk, Ewing, Overbeek, Ross (eds.) CADE 1988. LNCS, vol. 310, pp. 710\u2013713. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/BFb0012869","DOI":"10.1007\/BFb0012869"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Prior, A.N.: Logicians at play; or Syll, Simp and Hilbert. Australasian Journal of Philosophy 34(3), 182\u2013192 (1956). https:\/\/doi.org\/10.1080\/00048405685200181","DOI":"10.1080\/00048405685200181"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Prior, A.N.: Formal Logic. Clarendon Press, Oxford, 2nd edn. (1962). https:\/\/doi.org\/10.1093\/acprof:oso\/9780198241560.001.0001","DOI":"10.1093\/acprof:oso\/9780198241560.001.0001"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 27. pp. 495\u2013507. No. 11716 in LNAI, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Ulrich, D.: A legacy recalled and a tradition continued. J. Autom. Reasoning 27(2), 97\u2013122 (2001). https:\/\/doi.org\/10.1023\/A:1010683508225","DOI":"10.1023\/A:1010683508225"},{"key":"4_CR32","doi-asserted-by":"crossref","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. Michael Dunn on Information Based Logics, Outstanding Contributions to Logic, vol. 8, pp. 53\u201380. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-29300-4_4","DOI":"10.1007\/978-3-319-29300-4_4"},{"key":"4_CR33","unstructured":"Vampire Team: Vampire, online: https:\/\/vprover.github.io\/, accessed Feb 5, 2021"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Veroff, R.: Finding shortest proofs: An application of linked inference rules. J. Autom. Reasoning 27(2), 123\u2013139 (2001). https:\/\/doi.org\/10.1023\/A:1010635625063","DOI":"10.1023\/A:1010635625063"},{"key":"4_CR35","unstructured":"Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proc., vol. 1635, pp. 125\u2013138. CEUR-WS.org (2016), http:\/\/ceur-ws.org\/Vol-1635\/paper-11.pdf"},{"key":"4_CR36","doi-asserted-by":"crossref","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.) DECLARE 2019. LNCS (LNAI), vol. 12057, pp. 160\u2013177 (2020). https:\/\/doi.org\/10.1007\/978-3-030-46714-2_11","DOI":"10.1007\/978-3-030-46714-2_11"},{"key":"4_CR37","unstructured":"Wernhard, C., Bibel, W.: Learning from \u0141ukasiewicz and Meredith: Investigations into proof structures (extended version). CoRR abs\/2104.13645 (2021), https:\/\/arxiv.org\/abs\/2104.13645"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Woltzenlogel Paleo, B.: Atomic cut introduction by resolution: Proof structuring and compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol.\u00a06355, pp. 463\u2013480. Springer (2010). doi: https:\/\/doi.org\/10.1007\/978-3-642-17511-4_26","DOI":"10.1007\/978-3-642-17511-4_26"},{"key":"4_CR39","doi-asserted-by":"crossref","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 (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_109","DOI":"10.1007\/3-540-52885-7_109"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:21:20Z","timestamp":1625649680000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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","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":"5","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}