Confluence of cut-elimination procedures for the intuitionistic sequent calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationComputation and Logic in the Real World - Third Conference on Computability in Europe, CiE 2007, Proceedings
Pages398-407
Number of pages10
DOIs
Publication statusPublished - 2007 Dec 1
Event3rd Conference on Computability in Europe, CiE 2007 - Siena, Italy
Duration: 2007 Jun 182007 Jun 23

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4497 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other3rd Conference on Computability in Europe, CiE 2007
CountryItaly
CitySiena
Period07/6/1807/6/23

Keywords

  • Confluence
  • Cut-elimination
  • Explicit substitution
  • Sequent calculus
  • λ-calculus

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Confluence of cut-elimination procedures for the intuitionistic sequent calculus'. Together they form a unique fingerprint.

  • Cite this

    Kikuchi, K. (2007). Confluence of cut-elimination procedures for the intuitionistic sequent calculus. In Computation and Logic in the Real World - Third Conference on Computability in Europe, CiE 2007, Proceedings (pp. 398-407). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4497 LNCS). https://doi.org/10.1007/978-3-540-73001-9_41