Abstract
We present constructive arithmetic in Deduction modulo with rewrite rules only.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Crabbé, M.: Non-normalisation de la théorie de Zermelo, Manuscript (1974)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31, 33–72 (2003)
Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic 68(4), 1289–1316 (2003)
Dowek, G., Werner, B.: Arithmetic as a theory modulo, Manuscript (2004)
Dowek, G., Werner, B.: A constructive proof of Skolem theorem for constructive logic, Manuscript (2004)
Dowek, G.: La part du Calcul. Habilitation thesis, Université de Paris 7 (1999)
Girard, J.Y.: Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur, Thèse d’État, Université de Paris 7 (1972)
Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)
Gödel, K.: Über eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes, Dialectica 12, pp. 280-287 (1958); Reproduced in Feferman, S., et al. (eds.): Collected Works, vol. II, pp. 241–251. Oxford University Press, Oxford (1990)
Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121, 279–308 (1993)
Parigot, M.: Programming with proofs: A second order type theory. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 145–159. Springer, Heidelberg (1988)
Prawitz, D.: Natural deduction. A proof-theoretical study. Almqvist & Wiksell (1965)
Rasiowa, H., Sikorski, R.: The mathematics of metamathematics. Polish Scientific Publishers, Warsaw (1963)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dowek, G., Werner, B. (2005). Arithmetic as a Theory Modulo. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)