{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:31:06Z","timestamp":1783549866756,"version":"3.55.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031223365","type":"print"},{"value":"9783031223372","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_15","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"306-322","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Getting Saturated with\u00a0Induction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","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-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6353-952X","authenticated-orcid":false,"given":"Giles","family":"Reger","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":[[2022,12,29]]},"reference":[{"key":"15_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20\u201323. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_4"},{"key":"15_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/C2013-0-10412-6","author":"RS Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press (1988). https:\/\/doi.org\/10.1016\/C2013-0-10412-6","journal-title":"A Computational Logic Handbook. Academic Press"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., Harmelen, F.V., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62, 185\u2013253 (1993). https:\/\/doi.org\/10.1016\/0004-3702(93)90079-Q","journal-title":"Artif. Intell."},{"key":"15_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-24. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"15_CR6","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.) Superposition with Structural Induction. LNCS (LNAI), vol. 10483, pp. 172\u2013188. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10817-019-09519-x","volume":"64","author":"M Echenheim","year":"2020","unstructured":"Echenheim, M., Peltier, N.: Combining induction and saturation-based theorem proving. J. Automated Reasoning 64, 253\u2013294 (2020)","journal-title":"J. Automated Reasoning"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: 2021 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u201310 (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_34","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_34"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 123\u2013137. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-030-81097-9_9","volume-title":"Intelligent Computer Mathematics","author":"M Hajdu","year":"2021","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Inductive benchmarks for automated reasoning. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) CICM 2021. LNCS (LNAI), vol. 12833, pp. 124\u2013129. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81097-9_9"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-030-79876-5_21","volume-title":"Automated Deduction \u2013 CADE 28","author":"P Hozzov\u00e1","year":"2021","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Integer Induction in Saturation. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 361\u2013377. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_21"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Kersani, A., Peltier, N.: Combining superposition and induction: a practical realization. In: Proceedings of FroCoS, pp. 7\u201322 (2013)","DOI":"10.1007\/978-3-642-40885-4_2"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Castagna, G., Gordon, A.D. (eds.) POPL, pp. 260\u2013270 (2017). https:\/\/doi.org\/10.1145\/3093333.3009887","DOI":"10.1145\/3093333.3009887"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV, pp. 1\u201335. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 7, pp. 371\u2013443. North-Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-030-51054-1_30","volume-title":"Automated Reasoning","author":"G Passmore","year":"2020","unstructured":"Passmore, G., Cruanes, S., Ignatovich, D., Aitken, D., Bray, M., Kagan, E., Kanishev, K., Maclean, E., Mometto, N.: The Imandra automated reasoning system (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 464\u2013471. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_30"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: Fontaine, P. (ed.) CADE. pp. 477\u2013494. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_28"},{"key":"15_CR19","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":"15_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-28756-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Sonnex","year":"2012","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407\u2013421. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28"},{"issue":"2","key":"15_CR22","first-page":"99","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015-2018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019). https:\/\/doi.org\/10.3233\/SAT190123","DOI":"10.3233\/SAT190123"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:08:54Z","timestamp":1672358934000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}