{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T14:33:37Z","timestamp":1740148417805,"version":"3.37.3"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,7,18]],"date-time":"2016-07-18T00:00:00Z","timestamp":1468800000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000848","name":"University of Edinburgh","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000848","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1007\/s11786-016-0275-z","type":"journal-article","created":{"date-parts":[[2016,7,18]],"date-time":"2016-07-18T05:25:38Z","timestamp":1468819538000},"page":"429-457","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version)"],"prefix":"10.1007","volume":"10","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":[[2016,7,18]]},"reference":[{"key":"275_CR1","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: International Conference on Mathematical Knowledge Management, pp. 31\u201343. Springer, Berlin, Heidelberg (2006)","DOI":"10.1007\/11812289_4"},{"key":"275_CR2","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: International conference on interactive theorem proving, pp. 131\u2013146. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"275_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: International Joint Conference on Automated Reasoning, pp. 107\u2013121. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"275_CR4","doi-asserted-by":"crossref","DOI":"10.1142\/8027","volume-title":"A walk through combinatorics: an introduction to enumeration and graph theory","author":"M B\u00f3na","year":"2011","unstructured":"B\u00f3na, M.: A walk through combinatorics: an introduction to enumeration and graph theory. World scientific, Singapore (2011)"},{"key":"275_CR5","doi-asserted-by":"crossref","unstructured":"Bulwahn, L.: The new Quickcheck for Isabelle. In: International Conference on Certified Programs and Proofs, pp. 92\u2013108. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"275_CR6","doi-asserted-by":"crossref","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.T.: Little theories. In: International Conference on Automated Deduction, pp. 567\u2013581. Springer, Berlin, Heidelberg (1992)","DOI":"10.1007\/3-540-55602-8_192"},{"issue":"11","key":"275_CR7","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"9","author":"WM Farmer","year":"1993","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.T.: IMPS: an interactive mathematical proof system. J. Autom. Reasoning 9(11), 213\u2013248 (1993)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"275_CR8","doi-asserted-by":"crossref","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 specication and programming. J. ACM (JACM) 39(1), 95\u2013146 (1992)","journal-title":"J. ACM (JACM)"},{"key":"275_CR9","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: International Conference on Interactive Theorem Proving, pp. 100\u2013115. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"275_CR10","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M,: Constructive type classes in Isabelle. In: International Workshop on Types for Proofs and Programs, pp. 160\u2013174. Springer, Berlin, Heidelberg (2006)","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"275_CR11","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: International Conference on Certified Programs and Proofs, pp. 131\u2013146. Springer, Switzerland (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"275_CR12","unstructured":"Hurd, J.: System description: the Metis proof tactic. In: Benzm\u00fcller, C., Harrison, J., Sch\u00fcrmann, C. (eds.) Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), pp. 103\u2013104, Montego Bay (2005)"},{"issue":"2","key":"275_CR13","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BF02127748","volume":"18","author":"M Kerber","year":"1996","unstructured":"Kerber, M., Pr\u00e4cklein, A.: Using tactics to reformulate formulae for resolution theorem proving. Ann. Math. Artif. Intell. 18(2), 221\u2013241 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"275_CR14","doi-asserted-by":"crossref","unstructured":"Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: HOL with definitions: semantics, soundness, and a verified implementation. In: International Conference on Interactive Theorem Proving, pp. 308\u2013324. Springer, Switzerland (2014)","DOI":"10.1007\/978-3-319-08970-6_20"},{"key":"275_CR15","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O., Popescu, A.: A consistent foundation for Isabelle\/HOL. In: International Conference on Interactive Theorem Proving, pp. 234\u2013252. Springer, Switzerland (2015)","DOI":"10.1007\/978-3-319-22102-1_16"},{"issue":"1","key":"275_CR16","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"275_CR17","doi-asserted-by":"crossref","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set, HETS. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp, 519\u2013522. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-71209-1_40"},{"key":"275_CR18","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic, vol. 2283. Springer, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"275_CR19","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: 8th International Workshop on the Implementation of Logics, 2010. Invited talk"},{"issue":"1","key":"275_CR20","first-page":"41","volume":"2","author":"M Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reasoning 2(1), 41\u201362 (2009)","journal-title":"J. Formalized Reasoning"},{"key":"275_CR21","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511987045","volume-title":"A course in combinatorics","author":"JH Lint van","year":"2001","unstructured":"van Lint, J.H., Wilson, R.M.: A course in combinatorics. Cambridge University Press, Cambridge (2001)"},{"issue":"5","key":"275_CR22","doi-asserted-by":"crossref","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 Technol. Transfer 13(5), 419\u2013429 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"275_CR23","unstructured":"Zimmermann, T., Herbelin, H.: Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant. arXiv preprint, arXiv:1505.05028 (2015)"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-016-0275-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-016-0275-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-016-0275-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,11]],"date-time":"2019-09-11T05:20:07Z","timestamp":1568179207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-016-0275-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,18]]},"references-count":23,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["275"],"URL":"https:\/\/doi.org\/10.1007\/s11786-016-0275-z","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"type":"print","value":"1661-8270"},{"type":"electronic","value":"1661-8289"}],"subject":[],"published":{"date-parts":[[2016,7,18]]}}}