{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:25Z","timestamp":1779074485039,"version":"3.51.4"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030535179","type":"print"},{"value":"9783030535186","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_8","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"123-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Induction with Generalization in Superposition Reasoning"],"prefix":"10.1007","author":[{"given":"M\u00e1rton","family":"Hajd\u00fa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petra","family":"Hozzov\u00e1","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BFb0013063","volume-title":"Logic Programming and Automated Reasoning","author":"S Baker","year":"1992","unstructured":"Baker, S., Ireland, A., Smaill, A.: On the use of the constructive omega-rule within automated deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 214\u2013225. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0013063"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"8_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-319-94205-6_25","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2018","unstructured":"Blanchette, J.C., Peltier, N., Robillard, S.: Superposition with datatypes and codatatypes. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 370\u2013387. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_25"},{"key":"8_CR5","volume-title":"A Computational Logic Handbook, Perspectives incomputing","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, Perspectives incomputing, vol. 23. Academic Press, Cambridge (1979)"},{"issue":"6","key":"8_CR6","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177\u20131216 (2011)","journal-title":"J. Log. Comput."},{"issue":"2","key":"8_CR7","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., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62(2), 185\u2013253 (1993)","journal-title":"Artif. Intell."},{"key":"8_CR8","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: HipSpec: automating inductive proofs of program properties. In: Proceedings of the ATx\/WInG, pp. 16\u201325 (2012)"},{"key":"8_CR9","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":"8_CR10","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"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10817-019-09519-x","volume":"64","author":"M Echenim","year":"2019","unstructured":"Echenim, M., Peltier, N.: Combining induction and saturation-based theorem proving. J. Autom. Reason. 64(2), 253\u2013294 (2019). https:\/\/doi.org\/10.1007\/s10817-019-09519-x","journal-title":"J. Autom. Reason."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-31365-3_20","volume-title":"Automated Reasoning","author":"S Falke","year":"2012","unstructured":"Falke, S., Kapur, D.: Rewriting induction + linear arithmetic = decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 241\u2013255. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_20"},{"key":"8_CR13","unstructured":"Gleiss, B., Kov\u00e1cs, L., Robillard, S.: Loop analysis by quantification over iterations. In: Proceedings of the LPAR, pp. 381\u2013399 (2018)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-030-01090-4_15","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2018","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248\u2013266. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-40885-4_2","volume-title":"Frontiers of Combining Systems","author":"A Kersani","year":"2013","unstructured":"Kersani, A., Peltier, N.: Combining superposition and induction: a practical realization. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 7\u201322. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_2"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Proceedings of POPL, pp. 260\u2013270 (2017)","DOI":"10.1145\/3093333.3009887"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Passmore, G., et al.: The Imandra automated reasoning system. In: Proceedings of the IJCAR (2020, to appear)","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-030-29436-6_28","volume-title":"Automated Deduction \u2013 CADE 27","author":"G Reger","year":"2019","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 477\u2013494. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_28"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in Saturation-Based Proof Search. EasyChair Smart Slide (2020). https:\/\/easychair.org\/smart-slide\/slide\/hXmP","DOI":"10.29007\/snqj"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-21401-6_13","volume-title":"Automated Deduction - CADE-25","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (Co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 197\u2013213. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_13"},{"key":"8_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"},{"issue":"2","key":"8_CR23","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T Rybina","year":"2001","unstructured":"Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Trans. Comput. Log. 2(2), 155\u2013181 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR24","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"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"8_CR26","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"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T02:11:04Z","timestamp":1619230264000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","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":"35","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":"15","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":"9","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":"43% - 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":"3-4","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":"The conference was held virtually due to the COVID-19 pandemic.","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)"}}]}}