{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:02:51Z","timestamp":1771059771381,"version":"3.50.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030232498","type":"print"},{"value":"9783030232504","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_9","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T07:01:17Z","timestamp":1562050877000},"page":"125-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Lemma Discovery for Induction"],"prefix":"10.1007","author":[{"given":"Moa","family":"Johansson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-73595-3_16","volume-title":"Automated Deduction \u2013 CADE-21","author":"M Aderhold","year":"2007","unstructured":"Aderhold, M.: Improvements in formula generalization. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 231\u2013246. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-73595-3_16"},{"key":"9_CR2","unstructured":"Aubin, R.: Mechanizing structural induction. Ph.D. thesis, University of Edinburgh (1976)"},{"key":"9_CR3","first-page":"1","volume-title":"A Computational Logic","author":"ROBERT S. BOYER","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. ACM Monographs in Computer Science (1979)"},{"issue":"2","key":"9_CR4","first-page":"9","volume":"38","author":"B Buchberger","year":"2000","unstructured":"Buchberger, B.: Theory exploration with Theorema. Analele Universitatii Din Timisoara ser. Mat.-Informatica 38(2), 9\u201332 (2000)","journal-title":"Analele Universitatii Din Timisoara ser. Mat.-Informatica"},{"issue":"4","key":"9_CR5","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Log. 4(4), 470\u2013504 (2006). Towards Computer Aided Mathematics","journal-title":"J. Appl. Log."},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111\u2013120. Springer, Heidelberg (1988). \n                    https:\/\/doi.org\/10.1007\/BFb0012826"},{"key":"9_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-Level Guidance for Mathematical Reasoning","author":"A Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)"},{"key":"9_CR8","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). \n                    https:\/\/doi.org\/10.1007\/3-540-52885-7_123"},{"issue":"9","key":"9_CR9","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/357766.351266","volume":"35","author":"Koen Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP, pp. 268\u2013279 (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR10","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 2013. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"9_CR11","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). \n                    https:\/\/doi.org\/10.1007\/978-3-319-20615-8_23"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-13977-2_3","volume-title":"Tests and Proofs","author":"K Claessen","year":"2010","unstructured":"Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6\u201321. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-13977-2_3"},{"key":"9_CR13","volume-title":"Implementing Mathematics with the nuPRL Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M.: Implementing Mathematics with the nuPRL Development System. Prentice Hall, Upper Saddle River (1986)"},{"key":"9_CR14","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). \n                    https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30142-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"L Dixon","year":"2004","unstructured":"Dixon, L., Fleuriot, J.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83\u201398. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-30142-4_7"},{"key":"9_CR16","unstructured":"Dixon, L., Johansson, M.: IsaPlanner 2: a proof planner in Isabelle. DReaM Technical report (System description) (2007)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-319-99957-9_5","volume-title":"Artificial Intelligence and Symbolic Computation","author":"SH Einarsd\u00f3ttir","year":"2018","unstructured":"Einarsd\u00f3ttir, S.H., Johansson, M., \u00c5man\u00a0Pohjola, J.: Into the infinite - theory exploration for coinduction. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) AISC 2018. LNCS (LNAI), vol. 11110, pp. 70\u201386. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-99957-9_5"},{"key":"9_CR18","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: Initial experiments with statistical conjecturing over large formal corpora. In: Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 (CICM-WiP 2016). CEUR, vol. 1785, pp. 219\u2013228. CEUR-WS.org (2016)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-45221-5_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Heras","year":"2013","unstructured":"Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 389\u2013406. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-45221-5_27"},{"key":"9_CR20","unstructured":"Hesketh, J.: Using middle out reasoning to guide inductive theorem proving. Ph.D. thesis, University of Edinburgh (1992)"},{"key":"9_CR21","unstructured":"Hummel, B.: An investigation of formula generalization heuristics for inductive proofs. Interner Bericht Nr, 6\/87, Universit\u00e4t Karlsruhe (1987)"},{"key":"9_CR22","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reasoning 16, 79\u2013111 (1996)","journal-title":"J. Autom. Reasoning"},{"key":"9_CR23","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: an introduction to the hipster system. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 1\u201311. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-66107-0_1"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-17172-7_6","volume-title":"Verification, Induction, Termination Analysis","author":"M Johansson","year":"2010","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Dynamic rippling, middle-out reasoning and lemma discovery. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNCS (LNAI), vol. 6463, pp. 102\u2013116. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-17172-7_6"},{"issue":"3","key":"9_CR25","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M Johansson","year":"2011","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reasoning 47(3), 251\u2013289 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-08434-3_9","volume-title":"Intelligent Computer Mathematics","author":"M Johansson","year":"2014","unstructured":"Johansson, M., Ros\u00e9n, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 108\u2013122. Springer, Cham (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-08434-3_9"},{"issue":"2","key":"9_CR27","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reasoning 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/3-540-61511-3_112","volume-title":"Automated Deduction \u2014 Cade-13","author":"D Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 538\u2013552. Springer, Heidelberg (1996). \n                    https:\/\/doi.org\/10.1007\/3-540-61511-3_112"},{"key":"9_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Panagiotis, M., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-27940-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KRM Leino","year":"2012","unstructured":"Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315\u2013331. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-27940-9_21"},{"key":"9_CR31","unstructured":"Maclean, E.: Generalisation as a critic. Master\u2019s thesis, University of Edinburgh (1999)"},{"key":"9_CR32","unstructured":"McCasland, R., Bundy, A., Autexier, S.: Automated discovery of inductive theorems. In: Matuszewski, R., Rudnicki, P. (eds.) From Insight to Proof: Festschrift in Honor of A. Trybulec (2007)"},{"issue":"3","key":"9_CR33","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10489-017-0954-8","volume":"47","author":"R McCasland","year":"2017","unstructured":"McCasland, R., Bundy, A., Smith, P.: MATHsAiD: automated mathematical theory exploration. Appl. Intell. 47(3), 585\u2013606 (2017)","journal-title":"Appl. Intell."},{"issue":"2","key":"9_CR34","doi-asserted-by":"publisher","first-page":"1637","DOI":"10.1016\/j.eswa.2011.06.055","volume":"39","author":"O Montano-Rivas","year":"2012","unstructured":"Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based theorem discovery and concept invention. Expert Syst. Appl. 39(2), 1637\u20131646 (2012)","journal-title":"Expert Syst. Appl."},{"issue":"5","key":"9_CR35","first-page":"1505","volume":"4","author":"JS Moore","year":"2014","unstructured":"Moore, J.S., Wirth, C.-P.: Automation of mathematical induction as part of the history of logic. IfCoLog J. Log. Their Appl. 4(5), 1505\u20131634 (2014). SEKI-Report SR-2013-02","journal-title":"IfCoLog J. Log. Their Appl."},{"key":"9_CR36","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). \n                    https:\/\/doi.org\/10.1007\/978-3-319-96812-4_19"},{"key":"9_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"9_CR38","unstructured":"Papapanagiotou, P., Fleuriot, J.: The Boyer-Moore waterfall model revisited (2011). \n                    https:\/\/arxiv.org\/pdf\/1808.03810.pdf"},{"key":"9_CR39","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL-2010 (2010)"},{"key":"9_CR40","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). \n                    https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Smallbone, N., Johansson, M., Claessen, K., Algehed, M.: Quick specifications for the busy programmer. J. Funct. Program. 27, e18 (2017)","DOI":"10.1017\/S0956796817000090"},{"key":"9_CR42","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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28"},{"key":"9_CR43","unstructured":"Sonnex, W.: Fixed point promotion: taking the induction out of automated induction. Technical report UCAM-CL-TR-905, University of Cambridge, Computer Laboratory, March 2017"},{"key":"9_CR44","unstructured":"Wand, D.: Superposition: types and induction. Ph.D. thesis, Saarland University (2017)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T07:04:29Z","timestamp":1562051069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_9"}},"subtitle":["A Survey"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","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":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}