{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:25Z","timestamp":1725490105348},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74591-4_22","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T10:49:52Z","timestamp":1187779792000},"page":"294-301","source":"Crossref","is-referenced-by-count":2,"title":["Proof Pearl: Wellfounded Induction on the Ordinals Up to \u03b5 0"],"prefix":"10.1007","author":[{"given":"Matt","family":"Kaufmann","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Franzen, T.: Inexhaustibility, a non-exhaustive treatment. Lecture Notes in Logic, vol.\u00a016. A.K. Peters (2004)","DOI":"10.1201\/9781439863770"},{"key":"22_CR2","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: The consistency of elementary number theory. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics, North Holland, Amsterdam (1969)"},{"key":"22_CR3","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Provabillity and nonprovability of restricted transfinite induction in elementary number theory. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics, North Holland, Amsterdam (1969)"},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2268019","volume":"9","author":"R. Goodstein","year":"1944","unstructured":"Goodstein, R.: On the restricted ordinal theorem. Journal of Symbolic Logic\u00a09, 33\u201341 (1944)","journal-title":"Journal of Symbolic Logic"},{"key":"22_CR5","series-title":"ACM International Conference Proceeding Series","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1217975.1217984","volume-title":"Proceedings of ACL2 2006","author":"M.J.C. Gordon","year":"2006","unstructured":"Gordon, M.J.C., Hunt, W.A., Kaufmann, M., Reynolds, J.: An embedding of the ACL2 logic in HOL. In: Proceedings of ACL2 2006. ACM International Conference Proceeding Series, vol.\u00a0205, pp. 40\u201346. ACM Press, New York (2006)"},{"key":"22_CR6","first-page":"153","volume-title":"Proceedings of FMCAD 2006","author":"M.J.C. Gordon","year":"2006","unstructured":"Gordon, M.J.C., Hunt, W.A., Kaufmann, M., Reynolds, J.: An integration of HOL and ACL2. In: Proceedings of FMCAD 2006, pp. 153\u2013160. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"22_CR7","unstructured":"Huffman, B.: Countable ordinals. Isabelle Archive of Formal Proofs (November 2005)"},{"issue":"2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. Journal of Automated Reasoning\u00a026(2), 161\u2013203 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"22_CR9","unstructured":"Manolios, P., Vroon, D.: Ordinal arithmetic: Algorithms and mechanization. Journal of Automated Reasoning, 1\u201337 (2006)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T10:10:21Z","timestamp":1558260621000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540745907","9783540745914"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}