×

zbMATH — the first resource for mathematics

Proof normalization modulo. (English) Zbl 1059.03062
Summary: We define a generic notion of cut that applies to many first-order theories. We prove a generic cut-elimination theorem showing that the cut-elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church’s simple type theory.

MSC:
03F05 Cut-elimination and normal-form theorems
03B35 Mechanization of proofs and logical operations
Software:
Automath; Coq
PDF BibTeX XML Cite
Full Text: DOI Euclid
References:
[1] S.C. Bailin A normalization theorem for set theory , Journal of Symbolic Logic, vol. 53 (1988), no. 3, pp. 673–695. JSTOR: · Zbl 0683.03036 · doi:10.2307/2274565 · links.jstor.org
[2] H. Barendregt Lambda calculi with types , Handbook of logic in computer science (S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors), vol. 2, Oxford University Press,1992.
[3] R.S. Boyer and J.S. Moore A computational logic , Academic Press,1979. · Zbl 0448.68020
[4] A. Church A formulation of the simple theory of types , Journal of Symbolic Logic, vol. 5 (1940), no. 1, pp. 56–68. JSTOR: · Zbl 0023.28901 · links.jstor.org
[5] Th. Coquand and G. Huet The calculus of constructions , Information and Computation , vol. 76 (1988), pp. 95–120. · Zbl 0654.03045 · doi:10.1016/0890-5401(88)90005-3
[6] M. Crabbé Non-normalisation de ZF , Manuscript,1974.
[7] H.B. Curry An analysis of the logical substitution , American Journal of Mathematics , vol. 51 (1929), pp. 263–384. · JFM 55.0033.01
[8] G. Dowek Proof normalization for a first-order formulation of higher-order logic , Theorem proving in higher-order logics (E.L. Gunter and A. Felty, editors), Lecture Notes in Computer Science, vol. 1275, Springer-Verlag,1997, pp. 105–119. Rapport de Recherche 3383, Institut National de Recherche en Informatique et en Automatique , 1998. · Zbl 0905.03036
[9] G. Dowek, Th. Hardin, and C. Kirchner Theorem proving modulo , Journal of Automated Reasoning ,(to appear). · Zbl 1049.03011 · doi:10.1023/A:1027357912519
[10] J. Ekman Normal proofs in set theory , Doctoral thesis, Chalmers university of technology and University of Göteborg, 1994. · Zbl 0115.36603
[11] H.B. Enderton A mathematical introduction to logic , Academic Press,1972. · Zbl 0298.02002
[12] M.J. Fay First-order unification in an equational theory , Fourth workshop on automated deduction ,1979, pp. 161–167.
[13] J. Gallier Logic in computer science , Harper and Row,1986.
[14] J.Y. Girard Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur , Doctoral thesis, Université de Paris 7, 1972.
[15] J.Y. Girard, Y. Lafont, and P. Taylor Proofs and types , Cambridge University Press,1989. · Zbl 0671.68002
[16] L. Hallnäs On normalization of proofs in set theory , Doctoral thesis, University of Stockholm, 1983. · Zbl 0667.03041
[17] L. Henkin Banishing the rule of substitution for functional variables , Journal of Symbolic Logic, vol. 18 (1953), no. 3, pp. 201–208. JSTOR: · Zbl 0053.20003 · doi:10.2307/2267403 · links.jstor.org
[18] J.-M. Hullot Canonical forms and unification , Conference on automated deduction (W. Bibel and R. Kowalski, editors), Lecture Notes in Computer Science, vol. 87, Springer-Verlag,1980, pp. 318–334. · Zbl 0441.68108
[19] J.-L. Krivine and M. Parigot Programming with proofs , Journal of Information Processing and Cybernetics , vol. 26 (1990), no. 3, pp. 149–167. · Zbl 0699.68020
[20] P. Martin-Löf Intuitionistic type theory , Bibliopolis,1984.
[21] R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (editors) Selected papers on automath , Studies in Logic and the Foundations of Mathematics, vol. 133, North-Holland,1994.
[22] S. Owre and N.Shankar The formal semantics of PVS , Technical Report CSL-97-2R , SRI,1999. · Zbl 1165.68468
[23] Ch. Paulin-Mohring Inductive definitions in the system Coq - rules and properties , Typed lambda calculi and applications (M. Bezem and J.-F. Groote, editors), Lecture Notes in Computer Science, vol. 664, Springer-Verlag,1993, pp. 328–345. · Zbl 0844.68073
[24] G. Plotkin Building-in equational theories , Machine Intelligence , vol. 7 (1972), pp. 73–90. · Zbl 0262.68036
[25] D. Prawitz Natural deduction, a proof-theoretical study , Almqvist & Wiksell,1965. · Zbl 0173.00205
[26] M. Stickel Automated deduction by theory resolution , Journal of Automated Reasoning , vol. 4 (1985), no. 1, pp. 285–289. · Zbl 0616.68076 · doi:10.1007/BF00244275
[27] W.W. Tait Intensional interpretation of functionals of finite type I , Journal of Symbolic Logic, vol. 32 (1967), no. 2, pp. 198–212. JSTOR: · Zbl 0174.01202 · doi:10.2307/2271658 · links.jstor.org
[28] B. Werner Une théorie des constructions inductives , Doctoral thesis, Université Paris 7, 1994.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.