TY - GEN

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

AU - Kikuchi, Kentaro

PY - 2006/12/8

Y1 - 2006/12/8

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33845210199&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845210199&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:33845210199

SN - 3540482814

SN - 9783540482819

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 120

EP - 134

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings

T2 - 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006

Y2 - 13 November 2006 through 17 November 2006

ER -