Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
1999 | 46 | 1 | 179-225
Tytuł artykułu

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

Treść / Zawartość
Warianty tytułu
Języki publikacji
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}}$.
Słowa kluczowe
Opis fizyczny
  • LLAIC1, Université D'Auvergne, BP 86, 63172 Aubière Cedex, France
  • [Buch95] W. Buchholz, Proof-theoretic analysis of termination proofs, Annals of Pure and Applied Logic 75, 57-65, (1995).
  • [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).
  • [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).
  • [DJS95] V. Danos, J.-B. Joinet and H. Schellinx, A new deconstructive logic: Linear Logic, Preprint 936, Department of Mathematics, Utrecht University, (1995).
  • [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 $Γ_0$?, A Survey of Some Results in Proof Theory, Annals of Pure and Applied Logic, Vol. 53, 199-260, (1991).
  • [Gal93] J. Gallier, Constructive logics part I: a tutorial on proof systems and typed λ-calculi, Theoretical Computer Science, Vol. 110, 249-339, (1993).
  • [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).
  • [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).
  • [Hue80] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach. Vol. 27 (4), 797-821, (1980).
  • [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).
  • [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).
  • [Ros84] H. E. Rose, Subrecursion: functions and hierarchies, Clarendon Press, Oxford, (1984).
  • [Ros73] B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, Journal of the ACM, Vol. 20, 160-187, (1973).
  • [Sch51] K. Schütte, Beweistheoretische Erfassung der Unendlichen Induktion in der Zahlentheorie, Matematische Annalen, Vol. 122, 369-380, (1951).
  • [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)
  • [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).
Typ dokumentu
Identyfikator YADDA
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.