Logic Journal of IGPL Advance Access originally published online on August 8, 2009
Logic Journal of IGPL 2009 17(5):489-497; doi:10.1093/jigpal/jzp022
This article appears in the following Logic Journal of the IGPL issue: Special Issue: Logical and Semantical Frameworks with Applications [View the issue table of contents]
On the convergence of reduction-based and model-based methods in proof theory
École polytechnique and INRIA, LIX, École polytechnique, 91128 Palaiseau Cedex, France.
E-mail: gilles.dowek{at}polytechnique.edu
In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation.
Key Words: Cut elimination • reducibility candidates • models • truth values algebras
Received for publication 14 May 2008.
References
-
[1] Allali L. Algorithmic equality in Heyting arithmetic modulo. In: Higher Order Rewriting (2007).
[2] Andrews PB. Resolution in type theory. The Journal of Symbolic Logic (1971) 36(3):414–432.[CrossRef]
[3] Brauner P, Houtmann C, Kirchner C. Superdeduction at work. In: Rewriting, Computation and Proof, Essays dedicated to Jean-Pierre Jouannaud on the occasion of his 60th birthday (2007) Springer. 132–166. Lectures Notes in Computer Science 4600.
[4] Brauner P, Dowek G, Wack B. Normalization in supernatural deduction and in deduction modulo (2007) Manuscript.
[5] Cousineau D, Dowek G. Embedding Pure Types Systems in the lambda Pi-calculus modulo. In: Typed Lambda calculi and Applications (2007) Springer. 102–117. Lecture Notes in Computer Science 4583.
[6] Crabbé M. Non-normalisation de la théorie de Zermelo (1974) Manuscript.
[7] Crabbé M. Stratification and cut-elimination. The Journal of Symbolic Logic (1991) 56(1):213–226.[CrossRef]
[8] De Marco M, Lipton J. Completeness and cut-elimination in the intuitionistic theory of types. Journal of Logic and Computation (2005) 15:821–854.
[9] Dowek G. About folding-unfolding cuts and cuts modulo. Journal of Logic and Computation (2001) 11(3):419–429.
[10] Dowek G. Truth values algebras and proof normalization. In: TYPES 2006 (2007) Springer. Lectures Notes in Computer Science 4502.
[11] Dowek G, Hardin T, Kirchner C. Theorem proving modulo. Journal of Automated Reasoning (2003) 31:32–72.
[12] Dowek G, Hardin T, Kirchner C. HOL-lambda-sigma: an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science (2001) 11:1–25.[CrossRef]
[13] Dowek G, Hermant O. A simple proof that super-consistency implies cut elimination. Rewriting techniques and applications (2007) 96–106. Lecture Notes in Computer Science, 4533.
[14] Dowek G, Werner B. Proof normalization modulo. The Journal of Symbolic Logic (2003) 68(4):1289–1316.[CrossRef]
[15] Dowek G, Werner B. Arithmetic as a theory modulo. In: Term rewriting and applications (2005) Springer. 423–437. Lecture Notes in Computer Science 3467.
[16] Ekman J. Normal proofs in set theory (1994) Chalmers University of Technology and University of Göteborg. Doctoral thesis.
[17] Girard J-Y. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: 2nd Scandinavian Logic Symposium (1971) North-Holland. 63–92.
[18] Girard J-Y. Doctoral thesis. In: Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur (1972) 7. Université de Paris.
[19] Hallnäs L. On normalization of proofs in set theory (1983) University of Stockholm. Doctoral thesis.
[20] Hermant O. Méthodes sémantiques en déduction modulo (2005) 7. Université de Paris. Doctoral Thesis.
[21] Hermant O. Semantic cut elimination in the intuitionistic sequent calculus. In: Typed Lambda Calculi and Applications (2005) Springer. 221–233. Lectures Notes in Computer Science 3461.
[22] Okada M. A uniform semantic proof for cut elimination and completeness of various first and higher order logics. Theoretical Computer Science (2002) 281:471–498.[CrossRef][Web of Science]
[23] Parigot M. Strong normalization for the second order classical natural deduction. Logic in Computer Science (1993) 39–46.
[24] Prawitz D. Hauptsatz for higher order logic. The Journal of Symbolic Logic (1968) 33:452–457.[CrossRef]
[25] Prawitz D. Natural Deduction. A Proof-Theoretical Study (1965) Almqvist and Wiksell.
[26] Tait WW. A non constructive proof of Gentzen's Hauptsatz for second order predicate logic. Bulletin of the American Mathematical Society (1966) 72:980–983.[CrossRef][Web of Science]
[27] Tait WW. Intentional interpretations of functionals of finite type I. The Journal of Symbolic Logic (1967) 32:198–212.[CrossRef]
[28] Takahashi Mo. A proof of cut-elimination theorem in simple type theory. Journal of the Mathematical Society of Japan (1967) 19:399–410.[Web of Science]
[29] Wack B. Typage et déduction dans le calcul de réécriture. (2005) 1. Université Henri Poincaré Nancy. Doctoral Thesis.
[30] Werner B. Une théorie des constructions inductives. (1994) 7. Université de Paris. Doctoral Thesis.
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||