Arithmetic as a Theory Modulo

  • Gilles Dowek
  • Benjamin Werner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We present constructive arithmetic in Deduction modulo with rewrite rules only.


Predicate Logic Predicate Symbol Atomic Proposition Natural Deduction Proof Term 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Crabbé, M.: Non-normalisation de la théorie de Zermelo, Manuscript (1974)Google Scholar
  2. 2.
    Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31, 33–72 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic 68(4), 1289–1316 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Dowek, G., Werner, B.: Arithmetic as a theory modulo, Manuscript (2004)Google Scholar
  5. 5.
    Dowek, G., Werner, B.: A constructive proof of Skolem theorem for constructive logic, Manuscript (2004)Google Scholar
  6. 6.
    Dowek, G.: La part du Calcul. Habilitation thesis, Université de Paris 7 (1999)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)zbMATHGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121, 279–308 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Prawitz, D.: Natural deduction. A proof-theoretical study. Almqvist & Wiksell (1965)Google Scholar
  13. 13.
    Rasiowa, H., Sikorski, R.: The mathematics of metamathematics. Polish Scientific Publishers, Warsaw (1963)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Gilles Dowek
    • 1
  • Benjamin Werner
    • 1
  1. 1.Projet LogiCal, Pôle Commun de Recherche en Informatique du Plateau de Saclay, École polytechniqueINRIA, CNRS and Université de Paris-Sud, LIX, École polytechniquePalaiseau CedexFrance

Personalised recommendations