Name
Title | ||
|---|---|---|
Strong cut-elimination systems for hudelmaier's depth-bounded sequent calculus for implicational logic |
Abstract | ||
|---|---|---|
Inspired by the Curry-Howard correspondence, we study normalisation procedures in the depth-bounded intuitionistic sequent calculus of Hudelmaier (1988) for the implicational case, thus strengthening existing approaches to Cut-admissibility. We decorate proofs with terms and introduce various term-reduction systems representing proof transformations. In contrast to previous papers which gave different arguments for Cut-admissibility suggesting weakly normalising procedures for Cut-elimination, our main reduction system and all its variations are strongly normalising, with the variations corresponding to different optimisations, some of them with good properties such as confluence. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11814771_31 | IJCAR |
Keywords | Field | DocType |
normalisation procedure,implicational case,strong cut-elimination system,depth-bounded sequent calculus,depth-bounded intuitionistic sequent calculus,existing approach,curry-howard correspondence,weakly normalising procedure,different argument,implicational logic,different optimisations,main reduction system,good property,sequent calculus | Intuitionistic logic,Discrete mathematics,Natural deduction,Sequent calculus,Algorithm,Mathematical proof,Confluence,Cut-elimination theorem,Mathematics,Bounded function | Conference |
Volume | ISSN | ISBN |
4130 | 0302-9743 | 3-540-37187-7 |
Citations | PageRank | References |
0 | 0.34 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roy Dyckhoff | 1 | 452 | 49.09 |
| Delia Kesner | 2 | 369 | 39.75 |
| Stéphane Lengrand | 3 | 162 | 11.43 |