# Strong normalization proofs for cut elimination in Gentzen's sequent calculi

Banach Center Publications (1999)

- Volume: 46, Issue: 1, page 179-225
- ISSN: 0137-6934

## Access Full Article

top## Abstract

top## How to cite

topBittar, Elias. "Strong normalization proofs for cut elimination in Gentzen's sequent calculi." Banach Center Publications 46.1 (1999): 179-225. <http://eudml.org/doc/208921>.

@article{Bittar1999,

abstract = {We define an equivalent variant $LK_\{sp\}$ of the Gentzen sequent calculus $LK$. In $LK_\{sp\}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $_\{LK_\{sp\}\}$ by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation gives subrecursive bounds for the length of derivations. We give a strong normalization proof by applying orthogonal term rewriting results for a confluent restriction of the mix elimination system $_\{LK_\{sp\}\}$.},

author = {Bittar, Elias},

journal = {Banach Center Publications},

keywords = {cut elimination; strong normalization; term rewriting systems},

language = {eng},

number = {1},

pages = {179-225},

title = {Strong normalization proofs for cut elimination in Gentzen's sequent calculi},

url = {http://eudml.org/doc/208921},

volume = {46},

year = {1999},

}

TY - JOUR

AU - Bittar, Elias

TI - Strong normalization proofs for cut elimination in Gentzen's sequent calculi

JO - Banach Center Publications

PY - 1999

VL - 46

IS - 1

SP - 179

EP - 225

AB - We define an equivalent variant $LK_{sp}$ of the Gentzen sequent calculus $LK$. In $LK_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $_{LK_{sp}}$ by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation gives subrecursive bounds for the length of derivations. We give a strong normalization proof by applying orthogonal term rewriting results for a confluent restriction of the mix elimination system $_{LK_{sp}}$.

LA - eng

KW - cut elimination; strong normalization; term rewriting systems

UR - http://eudml.org/doc/208921

ER -

## References

top- [Buch95] W. Buchholz, Proof-theoretic analysis of termination proofs, Annals of Pure and Applied Logic 75, 57-65, (1995). Zbl0844.03031
- [CRS94] E. A. Cichon, M. Rusinowitch and S. Selhab, Cut elimination in sequent calculus and rewriting, Rapport CRIN 94-R-038, (1994).
- [CRS96] E. A. Cichon, M. Rusinowitch and S. Selhab, Cut elimination and rewriting: termination proofs, Submitted.
- [Der82] Dershowitz, Orderings for term rewriting systems, Theoretical Computer Science, Vol. 17 (5), 279-301, (1982). Zbl0525.68054
- [DJ90] N. Dershowitz and J. P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, J. Van Leeween (ed.), Vol. B, 243-320, Elsevier, Amsterdam, (1990). Zbl0900.68283
- [DJS95] V. Danos, J.-B. Joinet and H. Schellinx, A new deconstructive logic: Linear Logic, Preprint 936, Department of Mathematics, Utrecht University, (1995). Zbl0895.03023
- [DP96] R. Dyckhoff and L. Pinto, Cut-elimination in a permutation-free sequent calculus for intuitionistic logic, Submitted, (August-1996).
- [Dra88] A. G. Dragalin, Mathematical intuitionism, introduction to proof theory, Vol. 67 of Translations of Mathematical Monographs, 185-199, American Mathematical Society, (1988), (translation of an article that appeared in 1978).
- [Hon96] Hongwei Xi, On Weak and Strong Normalisations, Research report 96-189, Dept. of Mathematical Sciences Carnegie Mellon University, (1996).
- [Gal91] Gallier, What’s so Special about Kruskal’s Theorem and the Ordinal ${\Gamma}_{0}$?, A Survey of Some Results in Proof Theory, Annals of Pure and Applied Logic, Vol. 53, 199-260, (1991). Zbl0758.03025
- [Gal93] J. Gallier, Constructive logics part I: a tutorial on proof systems and typed λ-calculi, Theoretical Computer Science, Vol. 110, 249-339, (1993). Zbl0772.03026
- [Gen35] G. Gentzen, Investigations into logical deduction, in: Gentzen Collected Works, E. Szabo (ed.), North Holland, (1969).
- [Gen38] G. Gentzen, New version of the consistency proof of elementary number theory, in: Gentzen Collected Works, E. Szabo (ed.), North Holland, (1969).
- [Gir87] J. Y. Girard, Proof theory and logical complexity, Bibliopolis, (1987).
- [GLT89] J. Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge university press, (1989). Zbl0671.68002
- [Gra92] B. Gramlich, Relating innermost, weak, uniform and modular termination of term rewriting systems, in: International Conf. on Logic Programming and Automated Reasoning, St. Petersburg, A. Voronkov (ed.), Vol. 624, Lecture Notes in Artificial Intelligence, 285-296, Springer, (1992).
- [Gro93] Ph. de Groote, The conservation theorem revisited, in: International Conf. on Typed Lambda Calculi and applications, Vol. 664, Lecture Notes in Artificial Intelligence, 163-178, Springer, (1993).
- [Her95] H. Herbelin, Séquents qu'on calcule, Thèse de doctorat, Université Paris VII, (1995).
- [HL92] G. Huet and J.-J. Lévy. Computations In Orthogonal Rewrites Systems I, in: Computational Logic: Essays in Honour of Alan Robinson, J. Lassez and G. Plotkin (eds.), chapter 11, 395-414, MIT Press, Cambridge, Massachussets. (1992).
- [Hof92] D. Hofbauer, Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths, Theoretical Computer Science, Vol. 105 (1), 129-140, (1992). Zbl0759.68045
- [Hue80] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach. Vol. 27 (4), 797-821, (1980). Zbl0458.68007
- [Joi93] J. B. Joinet, Etude de la normalisation du calcul des séquents classique à travers la logique linéaire, Thèse de doctorat, Université Paris VII, (1993).
- [KW94] A. J. Kfoury and J. B. Wells, New notions of reduction and non-semantic proofs of β-strong normalization in typed λ-calculi, Technical Report 94-014, Computer Science Department, Boston University, (1994).
- [KL80] S. Kamin and J. J. Lévy, Two generalizations of the recursive path ordering, unpublished note, Dept. of Computer Science, Univ. of Illinois, Urbana, IL, (1980).
- [Klo80] J. W. Klop, Combinatory reduction systems, PH.D. thesis, CWI, Amsterdamm Mathematical Center Tracts N°. 127.
- [Klo92] J. W. Klop, Term Rewriting Systems, in: Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum (eds.), Vol. 2, chapter 1, 2-117, Clarendon Press, Oxford, (1992).
- [Kru60] J. B. Kruskal, Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture, Trans. Amer. Society, Vol. 95 210-225, (1960). Zbl0158.27002
- [Les90] P. Lescanne, Implementation of completion by transition rules + control: ORME, in: Proc. 2nd International Workshop on Algebraic and Logic Programming, Nancy, Vol. 463, Lectures Notes in Computer Science, 262-269, Springer, (1990).
- [MZ94] A. Middeldorp and H. Zantema, Simple Termination Revisited, in: Proc. of the 12th International Conference on Automated Deduction, CADE'94, Nancy, Lecture Notes in Artificial Intelligence 814, pp. 451-465, (1994).
- [Ned73] R. P. Nederpelt, Strong Normalization for a typed lambda calculus with lambda structured types, Ph.D. thesis, Tecnische Hogeschool Eindhoven, (1973).
- [O'D77] M. J. O'Donnell, Computing in systems described by equations, Lecture Notes in Computer Science, Vol. 58. Springer, Berlin, (1977).
- [Pab90] J.-F. Pabion, Cours de logique, D.E.A. Université Claude-Bernard, Lyon-1, (1990).
- [Par92] M. Parigot, λμ-calculus: an algorithmic interpretation of classical natural deduction, Lecture Notes in Computer Science, Vol. 624, 190-201, Springer, (1992).
- [Per82] L. C. P. D. Pereira, On the estimation of the length of normal derivations, Philosophical Studies 4, Akademilitteratur, Stockholm (1982).
- [Pfe94] F. Pfenning, A Structural proof of cut elimination and its representation in a logical framework, report CMU-CS-94-218, Carnegie Mellon University, (1994).
- [Pin93] L. Pinto, Cut formulae and logic programming, in: Extensions of Logic Programming, R. Dyckhoff (ed.), Lecture Notes in Artificial Intelligence, Vol. 798, 282-300, Springer, (1994).
- [Pra65] D. Prawitz, Natural deduction, a proof-theoretical study, Almquist & Wiskell, Stockholm (1965). Zbl0173.00205
- [Ros84] H. E. Rose, Subrecursion: functions and hierarchies, Clarendon Press, Oxford, (1984). Zbl0539.03018
- [Ros73] B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, Journal of the ACM, Vol. 20, 160-187, (1973). Zbl0267.68013
- [Sch51] K. Schütte, Beweistheoretische Erfassung der Unendlichen Induktion in der Zahlentheorie, Matematische Annalen, Vol. 122, 369-380, (1951). Zbl0042.00803
- [Tah92] E. Tahhan Bittar, Gentzen cut elimination for propositional sequent calculus by rewriting derivations, preprint Laboratoire de Logique, d'Algorithmique et d'Informatique de Clermont 1, N°. 16, (1992).
- [Tah94] E. Tahhan Bittar, Bornes recursives pour la terminaison d'algorithmes, thèse de doctorat, Université Lyon1, (1994).
- [Wei93] A. Weiermann, Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theoretical Computer Science, Vol. 139(1&2), 355-362, (1995) Zbl0874.68156
- [Wei94] A. Weiermann, Complexity Bounds for Some Finite Forms of Kruskal's Theorem, Journal of Symbolic Computation, Vol. 18 (5), 489-495, (1994).
- [Zan92] H. Zantema, Termination of Term Rewriting by Interpretation, technical report, Utrecht University, RUU-CS-92-14, (April-1992).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.