Name
Abstract | ||
|---|---|---|
We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3 ) are inter-permutable (using a set of basic “permutation reduction rules” derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1016/S0304-3975(98)00138-8 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
Intuitionistic logic,Natural deduction,Sequent calculus,intuitionistic sequent calculus,Proof theory | Journal | 212 |
Issue | ISSN | Citations |
1-2 | Theoretical Computer Science | 17 |
PageRank | References | Authors |
3.79 | 1 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roy Dyckhoff | 1 | 452 | 49.09 |
| Luis Pinto | 2 | 69 | 12.04 |