Confluence of cut-elimination procedures for the intuitionistic sequent calculus

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルComputation and Logic in the Real World - Third Conference on Computability in Europe, CiE 2007, Proceedings
ページ398-407
ページ数10
DOI
出版ステータスPublished - 2007 12月 1
イベント3rd Conference on Computability in Europe, CiE 2007 - Siena, Italy
継続期間: 2007 6月 182007 6月 23

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
4497 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other3rd Conference on Computability in Europe, CiE 2007
国/地域Italy
CitySiena
Period07/6/1807/6/23

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Confluence of cut-elimination procedures for the intuitionistic sequent calculus」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル