{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:03:20Z","timestamp":1771059800096,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031634970","type":"print"},{"value":"9783031634987","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We investigate how the automated inductive proof capabilities of the first-order prover Vampire can be improved by adding lemmas conjectured by the QuickSpec theory exploration system and by training strategy schedules specialized for inductive proofs. We find that adding lemmas improves performance (measured in number of proofs found for benchmark problems) by <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$40\\%$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>40<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> compared to Vampire\u2019s plain structural induction as baseline. Strategy training alone increases the number of proofs found by <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$130\\%$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>130<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, and the two methods in combination provide an increase of <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$183\\%$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>183<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>. By combining strategy training and lemma discovery we can prove more inductive benchmarks than previous state-of-the-art inductive proof systems (HipSpec and CVC4).<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_13","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"214-232","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Lemma Discovery and\u00a0Strategies for\u00a0Automated Induction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5445-3975","authenticated-orcid":false,"given":"S\u00f3lr\u00fan Halla","family":"Einarsd\u00f3ttir","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1097-8278","authenticated-orcid":false,"given":"Moa","family":"Johansson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2880-6121","authenticated-orcid":false,"given":"Nicholas","family":"Smallbone","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0989-5800","authenticated-orcid":false,"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Rewriting Techniques, pp. 1\u201330. Elsevier (1989)","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"13_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"B\u00e1rtek, F., Chvalovsk\u00fd, K., Suda, M.: Regularization in spider-style strategy discovery and schedule construction. In: IJCAR (2024), accepted","DOI":"10.1007\/978-3-031-63498-7_12"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Chv\u00e1tal, V.: A greedy heuristic for the set-covering problem. Math. Oper. Res. 4(3), 233\u2013235 (1979)","DOI":"10.1287\/moor.4.3.233"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-20615-8_23","volume-title":"Intelligent Computer Mathematics","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 333\u2013337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_23"},{"key":"13_CR7","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: The TIP format. http:\/\/tip-org.github.io\/format.html"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-66167-4_10","volume-title":"Frontiers of Combining Systems","author":"S Cruanes","year":"2017","unstructured":"Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172\u2013188. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10"},{"key":"13_CR9","unstructured":"Dixon, L., Johansson, M.: Isaplanner 2: A proof planner for isabelle (2007)"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Einarsd\u00f3ttir, S.H., Smallbone, N., Johansson, M.: Template-based theory exploration: Discovering properties of functional programs by testing. In: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages, IFL 2020, pp. 67-78. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3462172.3462192","DOI":"10.1145\/3462172.3462192"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Reger, G., Voronkov, A.: Getting Saturated with Induction, pp. 306\u2013322. Springer Nature Switzerland, Cham (2022)","DOI":"10.1007\/978-3-031-22337-2_15"},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-030-53518-6_8","volume-title":"Intelligent Computer Mathematics","author":"M Hajd\u00fa","year":"2020","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: Benzm\u00fcller, C., Miller, B. (eds.) Intelligent Computer Mathematics, pp. 123\u2013137. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8"},{"key":"13_CR13","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, 19-22 October 2021, pp. 1\u201310. IEEE (2021)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 299\u2013314. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_23"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-030-81097-9_8","volume-title":"Intelligent Computer Mathematics","author":"EK Holden","year":"2021","unstructured":"Holden, E.K., Korovin, K.: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) CICM 2021. LNCS (LNAI), vol. 12833, pp. 107\u2013123. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81097-9_8"},{"key":"13_CR16","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, 79\u2013111 (1996)","journal-title":"J. Autom. Reason."},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-23250-4_9","volume-title":"Intelligent Computer Mathematics","author":"M Johansson","year":"2019","unstructured":"Johansson, M.: Lemma discovery for induction. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 125\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_9"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: International Conference on Interactive Theorem Proving (2010)","DOI":"10.1007\/978-3-642-14052-5_21"},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, pp. 35\u201350. Springer, Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-319-21401-6_28","volume-title":"Automated Deduction - CADE-25","author":"G Reger","year":"2015","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 399\u2013415. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_28"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: CADE (2019). https:\/\/api.semanticscholar.org\/CorpusID:126940163","DOI":"10.29007\/snqj"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"13_CR23","unstructured":"Schurr, H.: Optimal strategy schedules for everyone. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), Haifa, Israel, 11 - 12 August, 2022. CEUR Workshop Proceedings, vol.\u00a03201. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3201\/paper8.pdf"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Smallbone, N.: Twee: An equational theorem prover. In: CADE, pp. 602\u2013613 (2021)","DOI":"10.1007\/978-3-030-79876-5_35"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Smallbone, N., Johansson, M., Claessen, K., Algehed, M.: Quick specifications for the busy programmer. J. Funct. Program. 27 (2017)","DOI":"10.1017\/S0956796817000090"},{"key":"13_CR26","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzac068","author":"G Sutcliffe","year":"2022","unstructured":"Sutcliffe, G.: The Logic Languages of the TPTP World. Logic J. IGPL (2022). https:\/\/doi.org\/10.1093\/jigpal\/jzac068","journal-title":"Logic J. IGPL"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BFb0054276","volume-title":"Automated Deduction \u2014 CADE-15","author":"T Tammet","year":"1998","unstructured":"Tammet, T.: Towards efficient subsumption. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 427\u2013441. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054276"},{"key":"13_CR28","unstructured":"Urban, J.: Blistr: The blind strategymaker. In: Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.) Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, 16-19 October 2015. EPiC Series in Computing, vol.\u00a036, pp. 312\u2013319. EasyChair (2015), https:\/\/easychair.org\/publications\/volume\/GCAI_2015"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"},{"key":"13_CR30","unstructured":"Voronkov, A.: Spider: learning in the sea of options. In: Vampire23: The 7th Vampire Workshop (2023), https:\/\/easychair.org\/smart-program\/Vampire23\/2023-07-05.html#talk:223833, to appear"},{"key":"13_CR31","unstructured":"Wolf, A., Letz, R.: Strategy parallelism in automated theorem proving. In: Cook, D.J. (ed.) Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference, May 18-20, 1998, Sanibel Island, Florida, USA, pp. 142\u2013146. AAAI Press (1998). http:\/\/www.aaai.org\/Library\/FLAIRS\/1998\/flairs98-027.php"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:27Z","timestamp":1747592247000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}