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

Kentaro Kikuchi

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

Kentaro Kikuchi

Systems & Software Division

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings
Pages	120-134
Number of pages	15
Publication status	Published - 2006 Dec 8
Event	13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006 - Phnom Penh, Cambodia Duration: 2006 Nov 13 → 2006 Nov 17

Publication series

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

Other

Other	13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006
Country	Cambodia
City	Phnom Penh
Period	06/11/13 → 06/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

Kikuchi, K. (2006). On a local-step cut-elimination procedure for the intuitionistic sequent calculus. In Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings (pp. 120-134). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4246 LNAI).

On a local-step cut-elimination procedure for the intuitionistic sequent calculus. / Kikuchi, Kentaro.

Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. 2006. p. 120-134 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4246 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kikuchi, K 2006, On a local-step cut-elimination procedure for the intuitionistic sequent calculus. in Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4246 LNAI, pp. 120-134, 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, Phnom Penh, Cambodia, 06/11/13.

Kikuchi, Kentaro. / On a local-step cut-elimination procedure for the intuitionistic sequent calculus. Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. 2006. pp. 120-134 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{75fb0f4ee1804f00b9884d691de84d18,

title = "On a local-step cut-elimination procedure for the intuitionistic sequent calculus",

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.",

author = "Kentaro Kikuchi",

year = "2006",

month = dec,

day = "8",

language = "English",

isbn = "3540482814",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "120--134",

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

note = "13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006 ; Conference date: 13-11-2006 Through 17-11-2006",

}

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 -