{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:15Z","timestamp":1725566655728},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_31","type":"book-chapter","created":{"date-parts":[[2010,9,27]],"date-time":"2010-09-27T20:20:02Z","timestamp":1285618802000},"page":"423-437","source":"Crossref","is-referenced-by-count":19,"title":["Arithmetic as a Theory Modulo"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"Crabb\u00e9, M.: Non-normalisation de la th\u00e9orie de Zermelo, Manuscript (1974)"},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031, 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"31_CR3","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Dowek, G., Werner, B.: Arithmetic as a theory modulo, Manuscript (2004)","DOI":"10.1007\/978-3-540-32033-3_31"},{"key":"31_CR5","unstructured":"Dowek, G., Werner, B.: A constructive proof of Skolem theorem for constructive logic, Manuscript (2004)"},{"key":"31_CR6","unstructured":"Dowek, G.: La part du Calcul. Habilitation thesis, Universit\u00e9 de Paris 7 (1999)"},{"key":"31_CR7","unstructured":"Girard, J.Y.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur, Th\u00e8se d\u2019\u00c9tat, Universit\u00e9 de Paris 7 (1972)"},{"key":"31_CR8","volume-title":"Proofs and Types","author":"J.Y. Girard","year":"1989","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)"},{"key":"#cr-split#-31_CR9.1","doi-asserted-by":"crossref","unstructured":"G??del, K.: ??ber eine bisher noch nicht ben??zte Erweiterung des finiten Standpunktes, Dialectica 12, pp. 280-287 (1958);","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"#cr-split#-31_CR9.2","unstructured":"Reproduced in Feferman, S., et al. (eds.): Collected Works, vol.??II, pp. 241???251. Oxford University Press, Oxford (1990)"},{"key":"31_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.-W. Klop","year":"1993","unstructured":"Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science\u00a0121, 279\u2013308 (1993)","journal-title":"Theoretical Computer Science"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/3-540-19027-9_10","volume-title":"ESOP \u201988","author":"M. Parigot","year":"1988","unstructured":"Parigot, M.: Programming with proofs: A second order type theory. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol.\u00a0300, pp. 145\u2013159. Springer, Heidelberg (1988)"},{"key":"31_CR12","unstructured":"Prawitz, D.: Natural deduction. A proof-theoretical study. Almqvist & Wiksell (1965)"},{"key":"31_CR13","volume-title":"The mathematics of metamathematics","author":"H. Rasiowa","year":"1963","unstructured":"Rasiowa, H., Sikorski, R.: The mathematics of metamathematics. Polish Scientific Publishers, Warsaw (1963)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:34:01Z","timestamp":1605742441000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}