{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:03:28Z","timestamp":1742943808309,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_16","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"246-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["SEPIA: Search for Proofs Using Inferred Automata"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Gransden","sequence":"first","affiliation":[]},{"given":"Neil","family":"Walkinshaw","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Raman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-28717-6_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Alama","year":"2012","unstructured":"Alama, J., K\u00fchlwein, D., Urban, J.: Automated and human proofs in general mathematics: an initial comparison. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 37\u201345. Springer, Heidelberg (2012)"},{"key":"16_CR2","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":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"16_CR3","unstructured":"Duncan, H.: The Use of Data Mining for the Automatic Formation of Tactics. Ph.d. thesis, University of Edinburgh (2007)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/978-3-319-08434-3_21","volume-title":"Intelligent Computer Mathematics","author":"T Gransden","year":"2014","unstructured":"Gransden, T., Walkinshaw, N., Raman, R.: Mining state-based models from proof corpora. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 282\u2013297. Springer, Heidelberg (2014)"},{"key":"16_CR5","unstructured":"Grov, G., Komendantskata, E., Bundy, A.: A Statistical Relational Learning Challenge Extracting Proof Strategies from Exemplar Proofs. In: ICML-12 Workshop on Statistical Relational Learning (2012)"},{"issue":"6","key":"16_CR6","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1093\/jigpal\/11.6.647","volume":"11","author":"M Jamnik","year":"2003","unstructured":"Jamnik, M., Kerber, M., Pollet, M., Benzm\u00fcller, C.: Automatic learning of proof methods in proof planning. Logic J. IGPL 11(6), 647\u2013673 (2003)","journal-title":"Logic J. IGPL"},{"key":"16_CR7","unstructured":"Kohavi, R.: A Study of Cross-validation and Bootstrap for Accuracy Estimation and Model Selection. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence, pp. 1137\u20131143. Morgan Kaufmann (1995)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Komendantskaya, E., Heras, J., Grov, G.: Machine learning in proof general: interfacing interfaces. In: User Interfaces for Theorem Provers, EPTCS, vol. 118, pp. 15\u201341 (2013)","DOI":"10.4204\/EPTCS.118.2"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0054059","volume-title":"Grammatical Inference","author":"KJ Lang","year":"1998","unstructured":"Lang, K.J., Pearlmutter, B.A., Price, R.A.: Results of the abbadingo one DFA learning competition and a new evidence-driven state merging algorithm. In: Honavar, V.G., Slutzki, G. (eds.) ICGI 1998. LNCS (LNAI), vol. 1433, pp. 1\u201312. Springer, Heidelberg (1998)"},{"key":"16_CR10","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.4. LogiCal Project. http:\/\/coq.inria.fr\/refman"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"4","key":"16_CR12","doi-asserted-by":"publisher","first-page":"791","DOI":"10.1007\/s10664-012-9210-3","volume":"18","author":"N Walkinshaw","year":"2013","unstructured":"Walkinshaw, N., Lambeau, B., Damas, C., Bogdanov, K., Dupont, P.: STAMINA: a competition to encourage the development and assessment of software model inference techniques. Empir. Softw. Eng. 18(4), 791\u2013824 (2013)","journal-title":"Empir. Softw. Eng."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Walkinshaw, N., Taylor, R., Derrick, J.: Inferring Extended Finite State Machine Models from Software Executions. Empir. Softw. Eng. 1\u201343 (2015)","DOI":"10.1007\/s10664-015-9367-7"},{"issue":"11","key":"16_CR14","first-page":"1408","volume":"55","author":"F Wiedijk","year":"2008","unstructured":"Wiedijk, F.: Formal proof - getting started. Not. AMS 55(11), 1408\u20131414 (2008)","journal-title":"Not. AMS"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:26:05Z","timestamp":1676467565000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}