On a local-step cut-elimination procedure for the intuitionistic sequent calculus

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

1 Citation (Scopus)

Abstract

In this paper we investigate, for intuitionistic implicational logic, the relationship between normalization in natural deduction and cut-elimination in a standard sequent calculus. First we identify a subset of proofs in the sequent calculus that correspond to proofs in natural deduction. Then we define a reduction relation on those proofs that exactly corresponds to normalization in natural deduction. The reduction relation is simulated soundly and completely by a cut-elimination procedure which consists of local proof transformations. It follows that the sequent calculus with our cut-elimination procedure is a proper extension that is conservative over natural deduction with normalization.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings
Pages120-134
Number of pages15
Publication statusPublished - 2006 Dec 8
Event13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006 - Phnom Penh, Cambodia
Duration: 2006 Nov 132006 Nov 17

Publication series

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

Other

Other13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006
CountryCambodia
CityPhnom Penh
Period06/11/1306/11/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'On a local-step cut-elimination procedure for the intuitionistic sequent calculus'. Together they form a unique fingerprint.

Cite this