{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:14:48Z","timestamp":1753888488874,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999562"},{"type":"electronic","value":"9783319999579"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99957-9_6","type":"book-chapter","created":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T08:26:31Z","timestamp":1534839991000},"page":"87-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Machine Learning for Inductive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Yaqing","family":"Jiang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petros","family":"Papapanagiotou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,22]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"issue":"1","key":"6_CR2","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Boulton, R.: Boyer-Moore automation for the HOL system. In: Higher Order Logic Theorem Proving and Its Applications, pp. 133\u2013142. Elsevier (1993)","DOI":"10.1016\/B978-0-444-89880-7.50015-2"},{"key":"6_CR4","series-title":"ACM Monograph Series","volume-title":"A Computational Logic","author":"R Boyer","year":"1979","unstructured":"Boyer, R., Moore, J.: A Computational Logic. ACM Monograph Series. Academic Press, Cambridge (1979)"},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TCIAIG.2012.2186810","volume":"4","author":"C Browne","year":"2012","unstructured":"Browne, C., et al.: A survey of Monte Carlo tree search methods. IEEE Trans. Comput. Intell. AI Games 4(1), 1\u201343 (2012)","journal-title":"IEEE Trans. Comput. Intell. AI Games"},{"key":"6_CR6","unstructured":"Bundy, A.: The automation of proof by mathematical induction. Technical report (1999)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: HipSpec: automating inductive proofs of program properties. In: ATx\/WInG@ IJCAR, pp. 16\u201325 (2012)","DOI":"10.29007\/3qwr"},{"key":"6_CR8","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). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"6_CR9","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"},{"key":"6_CR10","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 Moura de","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":"6_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.: IsaPlanner: a prototype proof planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279\u2013283. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_22"},{"key":"6_CR12","unstructured":"Dixon, L., Johansson, M.: IsaPlanner 2: a proof planner in Isabelle. DReaM Technical report (System description) (2007)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, vol. 46, pp. 125\u2013143 (2017)","DOI":"10.29007\/ntlb"},{"key":"6_CR14","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: Learning to prove with tactics. CoRR abs\/1804.00596 (2018). http:\/\/arxiv.org\/abs\/1804.00596"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","volume-title":"Automated Deduction \u2014 Cade-13","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 313\u2013327. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_97"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Heras, J., Komendantskaya, E.: ACL2(ml): machine-learning for ACL2. arXiv preprint arXiv:1404.3034 (2014)","DOI":"10.4204\/EPTCS.152.5"},{"key":"6_CR18","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). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_27"},{"issue":"3","key":"6_CR19","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. Reason. 47(3), 251\u2013289 (2011)","journal-title":"J. Autom. Reason."},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"1","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. Reason. 53, 1\u201341 (2014)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"6_CR21","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HoL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"6_CR22","series-title":"Advances in Formal Methods","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., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-1-4757-3188-0"},{"key":"6_CR23","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":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6"},{"issue":"1","key":"6_CR25","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41\u201357 (2009)","journal-title":"J. Appl. Log."},{"key":"6_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higherorder Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higherorder Logic, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"6_CR27","unstructured":"Papapanagiotou, P., Fleuriot, J.: The Boyer-Moore waterfall model revisited (2011)"},{"key":"6_CR28","doi-asserted-by":"crossref","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, vol. 1 (2010)","DOI":"10.29007\/36dt"},{"issue":"2, 3","key":"6_CR29","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E-A Brainiac theorem prover. AI Commun. 15(2, 3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"6_CR30","unstructured":"Scott, P.: Ordered geometry in Hilbert\u2019s Grundlagen der Geometrie. Ph.D. thesis, The University of Edinburgh (2015)"},{"key":"6_CR31","unstructured":"Urban, J.: BliStr: the blind strategymaker. arXiv preprint arXiv:1301.2683 (2013)"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99957-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T12:51:00Z","timestamp":1751806260000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99957-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999562","9783319999579"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99957-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}