{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:03:07Z","timestamp":1771059787129,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031424403","type":"print"},{"value":"9783031424410","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-42441-0_9","type":"book-chapter","created":{"date-parts":[[2023,8,29]],"date-time":"2023-08-29T16:05:28Z","timestamp":1693325128000},"page":"112-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Template-Based Conjecturing for\u00a0Automated Induction in\u00a0Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6693-5325","authenticated-orcid":false,"given":"Yutaka","family":"Nagashima","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7230-0131","authenticated-orcid":false,"given":"Zijin","family":"Xu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7775-436X","authenticated-orcid":false,"given":"Ningli","family":"Wang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2347-8037","authenticated-orcid":false,"given":"Daniel Sebastian","family":"Goc","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9345-3479","authenticated-orcid":false,"given":"James","family":"Bang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,8,30]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"Certified Programs and Proofs","author":"L Bulwahn","year":"2012","unstructured":"Bulwahn, L.: The new quickcheck for isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92\u2013108. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_10"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bundy, A., Basin, D.A., Hutter, D., Ireland, A.: Rippling - meta-level guidance for mathematical reasoning, Cambridge tracts in theoretical computer science, vol. 56. Cambridge University Press, Cambridge (2005)","DOI":"10.1017\/CBO9780511543326"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The OYSTER-CLAM system. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 647\u2013648. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_123"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: HipSpec: automating inductive proofs of program properties. In: Fleuriot, J.D., H\u00f6fner, P., McIver, A., Smaill, A. (eds.) ATx 2012\/WInG\u201912: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation, Manchester, UK, June 2012. EPiC Series in Computing, vol.\u00a017, pp. 16\u201325. EasyChair (2012). https:\/\/doi.org\/10.29007\/3qwr","DOI":"10.29007\/3qwr"},{"key":"9_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":"9_CR7","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: Chitil, O. (ed.) IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages, Virtual Event\/Canterbury, UK, 2-4 September 2020, pp. 67\u201378. ACM (2020). https:\/\/doi.org\/10.1145\/3462172.3462192","DOI":"10.1145\/3462172.3462192"},{"key":"9_CR8","unstructured":"Einarsd\u00f3ttir, S.H., Johansson, M., Smallbone, N.: LOL: A library of lemma templates for data-driven conjecturing. In: Buzzard, K., Kutsia, T. (eds.) Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics (CICM 2022) Informal Proceedings (2022). http:\/\/www3.risc.jku.at\/publications\/download\/risc_6584\/proceedings-CICM2022-informal.pdf#page=28"},{"key":"9_CR9","doi-asserted-by":"publisher","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, October 19-22, 2021, pp. 1\u201310. IEEE (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":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-66107-0_1","volume-title":"Interactive Theorem Proving","author":"M Johansson","year":"2017","unstructured":"Johansson, M.: Automated theory exploration for interactive theorem proving. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 1\u201311. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_1"},{"key":"9_CR11","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":"9_CR12","doi-asserted-by":"publisher","unstructured":"Kaufmann, M., Panagiotis Manolios, J.S.M. (ed.): Computer-Aided Reasoning ACL2 Case Studies. Advances in Formal Methods, Springer, New York, NY (2000). https:\/\/doi.org\/10.1007\/978-1-4757-3188-0","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-030-34175-6_14","volume-title":"Programming Languages and Systems","author":"Y Nagashima","year":"2019","unstructured":"Nagashima, Y.: LiFtEr: language to encode induction heuristics for Isabelle\/HOL. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 266\u2013287. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_14"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Nagashima, Y.: Smart induction for Isabelle\/HOL (tool paper). In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21-24 September 2020, pp. 245\u2013254. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_32","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_32"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Nagashima, Y.: Faster smarter proof by induction in Isabelle\/HOL. In: Zhou, Z. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event \/ Montreal, Canada, 19-27 August 2021, pp. 1981\u20131988. ijcai.org (2021). https:\/\/doi.org\/10.24963\/ijcai.2021\/273","DOI":"10.24963\/ijcai.2021\/273"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Nagashima, Y.: Definitional quantifiers realise semantic reasoning for proof by induction. In: Kov\u00e1cs, L., Meinke, K. (eds.) Tests and Proofs - 16th International Conference, TAP 2022, Held as Part of STAF 2022, Nantes, France, July 5, 2022, Proceedings, LNCS, vol. 13361, pp. 48\u201366. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-09827-7_4","DOI":"10.1007\/978-3-031-09827-7_4"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/978-3-319-63046-5_32","volume-title":"Automated Deduction \u2013 CADE 26","author":"Y Nagashima","year":"2017","unstructured":"Nagashima, Y., Kumar, R.: A proof strategy language and proof script generation for Isabelle\/HOL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 528\u2013545. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_32"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-319-96812-4_19","volume-title":"Intelligent Computer Mathematics","author":"Y Nagashima","year":"2018","unstructured":"Nagashima, Y., Parsert, J.: Goal-oriented conjecturing for\u00a0Isabelle\/HOL. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 225\u2013231. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_19"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"9_CR20","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., et al.: 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":"9_CR21","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011. EPiC Series in Computing, vol.\u00a02, pp. 1\u201311. EasyChair (2010). https:\/\/doi.org\/10.29007\/36dt","DOI":"10.29007\/36dt"},{"key":"9_CR22","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":"9_CR23","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"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42441-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,29]],"date-time":"2023-08-29T16:06:35Z","timestamp":1693325195000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-42441-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031424403","9783031424410"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-42441-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"30 August 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FSEN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamentals of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tehran","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iran","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 May 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fsen2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fsen.ir\/2023\/Default.aspx","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":"19","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":"9","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":"2","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":"47% - 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":"2","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)"}}]}}