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 -