{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:18:46Z","timestamp":1742962726842,"version":"3.40.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319206141"},{"type":"electronic","value":"9783319206158"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-20615-8_15","type":"book-chapter","created":{"date-parts":[[2015,6,22]],"date-time":"2015-06-22T15:31:23Z","timestamp":1434987083000},"page":"227-242","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automating Change of Representation for Proofs in Discrete Mathematics"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Raggi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gudmund","family":"Grov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alison","family":"Pease","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,23]]},"reference":[{"key":"15_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)"},{"key":"15_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565847","volume-title":"Gr\u00f6bner Bases and Applications","author":"B Buchberger","year":"1998","unstructured":"Buchberger, B., Winkler, F.: Gr\u00f6bner Bases and Applications, vol. 251. Cambridge University Press, Cambridge (1998)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction - CADE-11","author":"WM Farmer","year":"1992","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567\u2013581. Springer, Heidelberg (1992)"},{"issue":"11","key":"15_CR4","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"9","author":"WM Farmer","year":"1993","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 9(11), 213\u2013248 (1993)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM (JACM) 39(1), 95\u2013146 (1992)","journal-title":"J. ACM (JACM)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Heidelberg (2013)"},{"key":"15_CR7","unstructured":"Hurd, J.: System description: the Metis proof tactic. In: ESHOC, pp. 103\u2013104 (2005)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519\u2013522. Springer, Heidelberg (2007)"},{"key":"15_CR9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2013","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2013)"},{"key":"15_CR10","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. Practical Aspects of Automated Reasoning (PAAR), 5th International Joint Conference on Automated Reasoning (IJCAR) (2010)"},{"issue":"5","key":"15_CR11","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: new oracles for the HOL theorem prover. Int. J. Softw. Tools Tech. Transf. 13(5), 419\u2013429 (2011)","journal-title":"Int. J. Softw. Tools Tech. Transf."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-20615-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T15:22:23Z","timestamp":1674228143000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-20615-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319206141","9783319206158"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-20615-8_15","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":"23 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}