{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:36Z","timestamp":1759638996107,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,3,23]],"date-time":"2018-03-23T00:00:00Z","timestamp":1521763200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["VRG 12-004"],"award-info":[{"award-number":["VRG 12-004"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10817-018-9462-8","type":"journal-article","created":{"date-parts":[[2018,3,23]],"date-time":"2018-03-23T02:45:14Z","timestamp":1521773114000},"page":"95-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["On the Generation of Quantified Lemmas"],"prefix":"10.1007","volume":"63","author":[{"given":"Gabriel","family":"Ebner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6461-5982","authenticated-orcid":false,"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giselle","family":"Reis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,23]]},"reference":[{"key":"9462_CR1","unstructured":"Afshari, B., Hetzl, S., Leigh, G.E.: Herbrand disjunctions, cut elimination and context-free tree grammars. In: Altenkirch, T., (ed.) International Conference on Typed Lambda Calculi and Applications (TLCA) 2015, LIPIcs, vol.\u00a038, pp. 1\u201316. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"9462_CR2","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1515\/9781501502620-003","volume-title":"Concepts of Proof in Mathematics, Philosophy, and Computer Science","author":"B Afshari","year":"2016","unstructured":"Afshari, B., Hetzl, S., Leigh, G.E.: Herbrand confluence for first-order proofs with $$\\Pi _2$$ \u03a0 2 -cuts. In: Probst, D., Schuster, P. (eds.) Concepts of Proof in Mathematics, Philosophy, and Computer Science, pp. 5\u201340. De Gruyter, Berlin (2016)"},{"key":"9462_CR3","doi-asserted-by":"crossref","unstructured":"Afshari, B., Hetzl, S., Leigh, G.E.: On the Herbrand content of LK. In: Kohlenbach, U., van Bakel, S., Berardi,S., (eds.) 6th International Workshop on Classical Logic and Computation (CL&C 2016), EPTCS, vol.\u00a0213, pp. 1\u201310 (2016)","DOI":"10.4204\/EPTCS.213.1"},{"key":"9462_CR4","unstructured":"Afshari, B., Hetzl, S., Leigh G.E.: Herbrand\u2019s Theorem as Higher-Order Recursion. Preprint OWP-2018-01, Mathematisches Forschungsinstitut Oberwolfach (2018)"},{"key":"9462_CR5","doi-asserted-by":"crossref","unstructured":"Baaz, M., Zach, R.: Algorithmic structuring of cut-free proofs. In: Computer Science Logic (CSL) 1992. Lecture Notes in Computer Science, vol. 702, pp. 29\u201342. Springer (1993)","DOI":"10.1007\/3-540-56992-8_4"},{"key":"9462_CR6","volume-title":"Lattice Theory, American Mathematical Society Colloquium Publications","author":"G Birkhoff","year":"1967","unstructured":"Birkhoff, G.: Lattice Theory, American Mathematical Society Colloquium Publications, vol. XXV, 3rd edn. American Mathematical Society, Providence (1967)","edition":"3"},{"key":"9462_CR7","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1016\/B978-044450813-3\/50015-1","volume-title":"Handbook of Automated Reasoning","author":"A Bundy","year":"2001","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Voronkov, A., Robinson, J.A. (eds.) Handbook of Automated Reasoning, pp. 845\u2013911. Elsevier, Amsterdam (2001)"},{"key":"9462_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science","author":"A Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2005)"},{"issue":"5","key":"9462_CR9","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/s10958-009-9408-0","volume":"158","author":"S Cavagnetto","year":"2009","unstructured":"Cavagnetto, S.: The lengths of proofs: Kreisel\u2019s conjecture and G\u00f6dels speed-up theorem. J. Math. Sci. 158(5), 689\u2013707 (2009)","journal-title":"J. Math. Sci."},{"key":"9462_CR10","doi-asserted-by":"crossref","unstructured":"Colton, S.: Automated theory formation in pure mathematics. Ph.D. thesis, University of Edinburgh (2001)","DOI":"10.1007\/978-1-4471-0147-5"},{"key":"9462_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0147-5","volume-title":"Automated Theory Formation in Pure Mathematics","author":"S Colton","year":"2002","unstructured":"Colton, S.: Automated Theory Formation in Pure Mathematics. Springer, Berlin (2002)"},{"issue":"4","key":"9462_CR12","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3127401","volume":"18","author":"S Eberhard","year":"2017","unstructured":"Eberhard, S., Ebner, G., Hetzl, S.: Algorithmic compression of finite tree languages by rigid acyclic grammars. ACM Trans. Comput. Log. 18(4), 26:1\u201326:20 (2017)","journal-title":"ACM Trans. Comput. Log."},{"issue":"6","key":"9462_CR13","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1016\/j.apal.2015.01.002","volume":"166","author":"S Eberhard","year":"2015","unstructured":"Eberhard, S., Hetzl, S.: Inductive theorem proving based on tree grammars. Ann. Pure Appl. Log. 166(6), 665\u2013700 (2015)","journal-title":"Ann. Pure Appl. Log."},{"key":"9462_CR14","doi-asserted-by":"crossref","unstructured":"Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: 8th International Joint Conference on Automated Reasoning, IJCAR (2016)","DOI":"10.1007\/978-3-319-40229-1_20"},{"issue":"5\u20136","key":"9462_CR15","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1093\/jigpal\/jzm040","volume":"15","author":"M Finger","year":"2007","unstructured":"Finger, M., Gabbay, D.: Equal rights for the cut: computable non-analytic cuts in cut-based proofs. Log. J. IGPL 15(5\u20136), 553\u2013575 (2007)","journal-title":"Log. J. IGPL"},{"key":"9462_CR16","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39, 176\u2013210,405\u2013431 (1934\u20131935)","DOI":"10.1007\/BF01201363"},{"key":"9462_CR17","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Leitsch, A., Reis, G., Tapolczai, J., Weller, D.: Introducing quantified cuts in logic with equality. In: Demri, S., Kapur, D., Weidenbach, C., (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR. Lecture Notes in Computer Science, vol. 8562, pp. 240\u2013254. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_17"},{"key":"9462_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2014.05.018","volume":"549","author":"S Hetzl","year":"2014","unstructured":"Hetzl, S., Leitsch, A., Reis, G., Weller, D.: Algorithmic introduction of quantified cuts. Theor. Comput. Sci. 549, 1\u201316 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9462_CR19","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18). Lecture Notes in Computer Science, vol.\u00a07180, pp. 228\u2013242. Springer (2012)","DOI":"10.1007\/978-3-642-28717-6_19"},{"issue":"1\u20132","key":"9462_CR20","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1\u20132), 79\u2013111 (1996)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9462_CR21","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M Johansson","year":"2011","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251\u2013289 (2011)","journal-title":"J. Autom. Reason."},{"key":"9462_CR22","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.tcs.2017.10.003","volume":"706","author":"A Leitsch","year":"2018","unstructured":"Leitsch, A., Lettmann, M.P.: The problem of $$\\Pi _2$$ \u03a0 2 -cut-introduction. Theor. Comput. Sci. 706, 83\u2013116 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"9462_CR23","doi-asserted-by":"crossref","unstructured":"Miller, D., Nigam, V.: Incorporating tables into proofs. In: 16th Conference on Computer Science and Logic (CSL07). Lecture Notes in Computer Science, vol.\u00a04646, pp. 466\u2013480. Springer (2007)","DOI":"10.1007\/978-3-540-74915-8_35"},{"key":"9462_CR24","first-page":"137","volume":"88","author":"V Orevkov","year":"1979","unstructured":"Orevkov, V.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta 88, 137\u2013161 (1979)","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta"},{"issue":"1","key":"9462_CR25","first-page":"153","volume":"5","author":"GD Plotkin","year":"1970","unstructured":"Plotkin, G.D.: A note on inductive generalization. Mach. Intell. 5(1), 153\u2013163 (1970)","journal-title":"Mach. Intell."},{"key":"9462_CR26","first-page":"101","volume":"6","author":"GD Plotkin","year":"1971","unstructured":"Plotkin, G.D.: A further note on inductive generalization. Mach. Intell. 6, 101\u2013124 (1971)","journal-title":"Mach. Intell."},{"key":"9462_CR27","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1016\/S0049-237X(98)80023-2","volume-title":"Handbook of Proof Theory","author":"P Pudl\u00e1k","year":"1998","unstructured":"Pudl\u00e1k, P.: The Lengths of Proofs. In: Buss, S. (ed.) Handbook of Proof Theory, pp. 547\u2013637. Elsevier, Amsterdam (1998)"},{"issue":"1","key":"9462_CR28","first-page":"135","volume":"5","author":"JC Reynolds","year":"1970","unstructured":"Reynolds, J.C.: Transformational systems and the algebraic structure of atomic formulas. Mach. Intell. 5(1), 135\u2013151 (1970)","journal-title":"Mach. Intell."},{"key":"9462_CR29","volume-title":"Mathematical Logic","author":"JR Shoenfield","year":"1973","unstructured":"Shoenfield, J.R.: Mathematical Logic, 2nd edn. Addison Wesley, Boston (1973)","edition":"2"},{"issue":"2","key":"9462_CR30","first-page":"319","volume":"49","author":"V Sorge","year":"2008","unstructured":"Sorge, V., Colton, S., McCasland, R., Meier, A.: Classification results in quasigroup and loop theory via a combination of automated reasoning tools. Comment. Math. Univ. Carol. 49(2), 319\u2013339 (2008)","journal-title":"Comment. Math. Univ. Carol."},{"issue":"2\u20133","key":"9462_CR31","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-007-9093-y","volume":"40","author":"V Sorge","year":"2008","unstructured":"Sorge, V., Meier, A., McCasland, R., Colton, S.: Automatic construction and verification of isotopy invariants. J. Autom. Reason. 40(2\u20133), 221\u2013243 (2008)","journal-title":"J. Autom. Reason."},{"key":"9462_CR32","first-page":"104","volume":"75","author":"R Statman","year":"1979","unstructured":"Statman, R.: Lower bounds on Herbrand\u2019s theorem. Proc. Am. Math. Soc. 75, 104\u2013107 (1979)","journal-title":"Proc. Am. Math. Soc."},{"issue":"4","key":"9462_CR33","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. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9462_CR34","doi-asserted-by":"crossref","unstructured":"Vysko\u010dil, J., Stanovsk\u00fd, D., Urban, J.: Automated proof compression by invention of new definitions. In: Clark, E.M., Voronkov, A., (eds.) Logic for Programming, Artifical Intelligence and Reasoning (LPAR-16). Lecture Notes in Computer Science, vol. 6355, pp. 447\u2013462. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_25"},{"key":"9462_CR35","doi-asserted-by":"crossref","unstructured":"Woltzenlogel\u00a0Paleo, B.: Atomic cut introduction by resolution: proof structuring and compression. In: Clark, E.M., Voronkov, A., (eds.) Logic for Programming, Artifical Intelligence and Reasoning (LPAR-16). Lecture Notes in Computer Science, vol. 6355, pp. 463\u2013480. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_26"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9462-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9462-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9462-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,16]],"date-time":"2022-08-16T19:44:42Z","timestamp":1660679082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9462-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,23]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["9462"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9462-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,3,23]]},"assertion":[{"value":"16 January 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 March 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}