Abstract
We prove confluence of two cut-elimination procedures for the implicational fragment of a standard intuitionistic sequent calculus. One of the cut-elimination procedures uses global proof transformations while the other consists of local ones. Both of them include permutation of cuts to simulate β-reduction in an isomorphic image of the λ-calculus. We establish the confluence properties through a conservativity result on the cut-elimination procedures.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bloo, R., Geuvers, H.: Explicit substitution: On the edge of strong normalization. Theoretical Computer Science 211, 375–395 (1999)
Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. The Journal of Symbolic Logic 62, 755–807 (1997)
Espírito Santo, J.: Revisiting the correspondence between cut elimination and normalisation. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 600–611. Springer, Heidelberg (2000)
Gentzen, G.: Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, 39: pp. 176–210, pp. 405–431, English translation in [9 pp. 68–131] (1935)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Hardin, T.: Résultats de confluence pour les règles fortes de la logique combinatoire catégorique et liens avec les lambda-calculs. Thèse de doctorat, Université de Paris VII (1987)
Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479–490. Academic Press, San Diego (1980)
Kikuchi, K.: On a local-step cut-elimination procedure for the intuitionistic sequent calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 120–134. Springer, Heidelberg (2006)
Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam (1969)
Takahashi, M.: Parallel reductions in λ-calculus. Information and Computation 118, 120–127 (1995)
Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. Fundamenta Informaticae 45, 123–155 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kikuchi, K. (2007). Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds) Computation and Logic in the Real World. CiE 2007. Lecture Notes in Computer Science, vol 4497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73001-9_41
Download citation
DOI: https://doi.org/10.1007/978-3-540-73001-9_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73000-2
Online ISBN: 978-3-540-73001-9
eBook Packages: Computer ScienceComputer Science (R0)