{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:07:31Z","timestamp":1742954851781,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_12","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"183-199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Model for Capturing and Replaying Proof Strategies"],"prefix":"10.1007","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cliff B.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrius","family":"Velykis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iain","family":"Whiteside","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"issue":"4","key":"12_CR1","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/j.scico.2008.09.014","volume":"74","author":"A Butterfield","year":"2009","unstructured":"Butterfield, A., Freitas, L., Woodcock, J.: Mechanising a formal model of flash memory. Sci. Comp. Prog. 74(4), 219\u2013237 (2009)","journal-title":"Sci. Comp. Prog."},{"key":"12_CR2","unstructured":"Freitas, L., Jones, C.B., Velykis, A.: Can a system learn from interactive proofs?. In: Voronkov, A., Korovina, M. (eds.) HOWARD-60. A Festschrift on the Occasion of Howard Barringer\u2019s 60th Birthday, pp. 124\u2013139. EasyChair (2014)"},{"key":"12_CR3","unstructured":"Freitas, L., Jones, C.B., Velykis, A., Whiteside, I.: How to say why. Technical report CS-TR-1398, Newcastle University, November 2013. www.ai4fm.org\/tr"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s00165-007-0059-y","volume":"20","author":"L Freitas","year":"2008","unstructured":"Freitas, L., Woodcock, J.: Mechanising mondex with Z\/Eves. Formal Aspects Comput. 20(1), 117\u2013139 (2008)","journal-title":"Formal Aspects Comput."},{"issue":"2\u20133","key":"12_CR5","first-page":"357","volume":"3","author":"L Freitas","year":"2009","unstructured":"Freitas, L., Woodcock, J.: A chain datatype in Z. Int. J. Softw. Inform. 3(2\u20133), 357\u2013374 (2009)","journal-title":"Int. J. Softw. Inform."},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-319-06410-9_20","volume-title":"FM 2014: Formal Methods","author":"L Freitas","year":"2014","unstructured":"Freitas, L., Whiteside, I.: Proof Patterns for Formal Methods. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 279\u2013295. Springer, Heidelberg (2014)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Grov, G., Kissinger, A., Lin, Y.: A graphical language for proof strategies. In: McMillan et al. [MMV13], pp. 324\u2013339","DOI":"10.1007\/978-3-642-45221-5_23"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39320-4_28","volume-title":"Intelligent Computer Mathematics","author":"J Heras","year":"2013","unstructured":"Heras, J., Komendantskaya, E.: ML4PG in computer algebra verification. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 354\u2013358. Springer, Heidelberg (2013)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in acl2. In: McMillan et al. [MMV13], pp. 389\u2013406","DOI":"10.1007\/978-3-642-45221-5_27"},{"issue":"3","key":"12_CR10","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":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-39698-4_14","volume-title":"Theories of Programming and Formal Methods","author":"CB Jones","year":"2013","unstructured":"Jones, C.B., Freitas, L., Velykis, A.: Ours Is to reason why. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 227\u2013243. Springer, Heidelberg (2013)"},{"key":"12_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3180-9","volume-title":"mural: A Formal Development Support System","author":"CB Jones","year":"1991","unstructured":"Jones, C.B., Jones, K.D., Lindsay, P.A., Moore, R.: mural: A Formal Development Support System. Springer, London (1991)"},{"volume-title":"Case Studies in Systematic Software Development","year":"1990","key":"12_CR13","unstructured":"Jones, C.B., Shaw, R.C.F. (eds.): Case Studies in Systematic Software Development. Prentice Hall International, Englewood (1990)"},{"key":"12_CR14","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. CoRR, abs\/1402.3578 (2014)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","year":"2013","unstructured":"McMillan, K., Middeldorp, A., Voronkov, A. (eds.): LPAR-19 2013. LNCS, vol. 8312. Springer, Heidelberg (2013)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle: A Generic Theorem Prover","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72\u201385. Springer, Heidelberg (1997)"},{"key":"12_CR18","unstructured":"Velykis, A.: Inferring the proof process. In: Choppy, C., et al. (eds.) FM2012 Doctoral Symposium, Paris, France, August 2012"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,14]],"date-time":"2023-02-14T23:10:34Z","timestamp":1676416234000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}