{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:01:27Z","timestamp":1770289287996,"version":"3.49.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"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>Integers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover <jats:sc>Vampire<\/jats:sc> and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_21","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"361-377","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Integer Induction in Saturation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0845-5811","authenticated-orcid":false,"given":"Petra","family":"Hozzov\u00e1","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. of CAV. LNCS, vol. 6806, pp. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"21_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"21_CR3","doi-asserted-by":"publisher","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.) Proc. of CICM. LNCS, vol. 9150, pp. 333\u2013337. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_23","DOI":"10.1007\/978-3-319-20615-8_23"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating Inductive Proofs using Theory Exploration. In: Bonacina, M.P. (ed.) Proc. of CADE. LNCS, vol. 7898, pp. 392\u2013406. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Cruanes, S.: Superposition with Structural Induction. In: Dixon, C., Finger, M. (eds.) Proc. of FRoCoS. LNCS, vol. 10483, pp. 172\u2013188. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10","DOI":"10.1007\/978-3-319-66167-4_10"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proc. of TACAS. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"21_CR7","doi-asserted-by":"publisher","unstructured":"Dixon, L., Fleuriot, J.: Higher Order Rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) Proc. of TPHOLs. LNCS, vol. 3223, pp. 83\u201398. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30142-4_7","DOI":"10.1007\/978-3-540-30142-4_7"},{"key":"21_CR8","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified Invariants via Syntax-Guided Synthesis. In: Dillig, I., Tasiran, S. (eds.) Proc. of CAV. LNCS, vol. 11561, pp. 259\u2013277. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Georgiou, P., Gleiss, B., Kov\u00e1cs, L.: Trace Logic for Inductive Loop Reasoning. In: Ivrii, A., Strichman, O. (eds.) Proc. of FMCAD. Conference Series: FMCAD, vol. 1, pp. 255\u2013263 (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_33","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_33"},{"key":"21_CR10","doi-asserted-by":"publisher","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.) Proc. of CICM. LNCS, vol. 12236, pp. 123\u2013137. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach, vol. 3. Springer (06 2000). https:\/\/doi.org\/10.1007\/978-1-4615-4449-4","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"21_CR12","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.) Proc. of POPL. ACM SIGPLAN Notices, vol. 52, pp. 260\u2013270. ACM (2017). https:\/\/doi.org\/10.1145\/3093333.3009887","DOI":"10.1145\/3093333.3009887"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Proc. of CAV. LNCS, vol. 8044, pp. 1\u201335. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Passmore, G., Cruanes, S., Ignatovich, D., Aitken, D., Bray, M., Kagan, E., Kanishev, K., Maclean, E., Mometto, N.: The Imandra Automated Reasoning System. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proc. of IJCAR. LNCS, vol. 12167, pp. 464\u2013471. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_30","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Reger, G., Schoisswohl, J., Voronkov, A.: Making Theory Reasoning Simpler. In: Groote, J.F., Larsen, K. (eds.) Proc. of TACAS. LNCS, vol. 12652, pp. 164\u2013180. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_9","DOI":"10.1007\/978-3-030-72013-1_9"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Reger, G., Voronkov, A.: Induction in Saturation-Based Proof Search. In: Fontaine, P. (ed.) Proc. of CADE. LNCS, vol. 11716, pp. 477\u2013494. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_28","DOI":"10.1007\/978-3-030-29436-6_28"},{"key":"21_CR17","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT Solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) Proc. of VMCAI. LNCS, vol. 8931, pp. 80\u201398. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: An Automated Prover for Properties of Recursive Data Structures. In: Flanagan, C., K\u00f6nig, B. (eds.) Proc. of TACAS. LNCS, vol. 7214, pp. 407\u2013421. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Voronkov, A.: AVATAR: The Architecture for First-Order Theorem Provers. In: Biere, A., Bloem, R. (eds.) Proc. of CAV. LNCS, vol. 8559, pp. 696\u2013710. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","DOI":"10.1007\/978-3-319-08867-9_46"}],"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_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:30:35Z","timestamp":1625650235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}