{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:29:57Z","timestamp":1784845797415,"version":"3.55.0"},"publisher-location":"Cham","reference-count":14,"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>Proof by induction is commonplace in modern mathematics and computational logic. This paper overviews and discusses our recent results in turning saturation-based first-order theorem proving into a powerful framework for automating inductive reasoning. We formalize applications of induction as new inference rules of the saturation process, add instances of appropriate induction schemata to the search space, and use these rules and instances immediately upon their addition for the purpose of guiding induction. Our results show, for example, that many problems from formal verification and mathematical theories can now be solved completely automatically using a first-order theorem prover.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_2","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"21-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Induction in\u00a0Saturation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0845-5811","authenticated-orcid":false,"given":"Petra","family":"Hozzov\u00e1","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"2_CR1","volume-title":"A Computational Logic Handbook","author":"RS Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Cook, B.: Formal reasoning about the security of Amazon web services. In: CAV, pp. 38\u201347 (2018)","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Cruanes, S.: Superposition with structural induction. In: FroCoS (2017)","DOI":"10.1007\/978-3-319-66167-4_10"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: CICM (2020)","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"2_CR5","unstructured":"Hajdu, M., Kov\u00e1cs, L., Rawson, M.: Rewriting and inductive reasoning. In: LPAR (2024, to appear)"},{"key":"2_CR6","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: FMCAD (2021)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Integer induction in saturation. In: CADE, pp. 361\u2013377 (2021)","DOI":"10.1007\/978-3-030-79876-5_21"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: POPL, pp. 260\u2013270 (2017)","DOI":"10.1145\/3009837.3009887"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Continuous reasoning: scaling the impact of formal methods. In: LICS, pp. 13\u201325 (2018)","DOI":"10.1145\/3209108.3209109"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., et al.: The Imandra automated reasoning system (system description). In: IJCAR, pp. 464\u2013471 (2020)","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: CADE (2019)","DOI":"10.29007\/snqj"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: VMCAI, pp. 80\u201398 (2015)","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"2_CR14","unstructured":"Wand, D.: Superposition: types and induction. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2017). https:\/\/tel.archives-ouvertes.fr\/tel-01592497"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:13Z","timestamp":1747592233000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_2","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"}}]}}