Name
Abstract | ||
|---|---|---|
We investigate cut elimination in multi-focused sequent calculi and the impact on the cut elimination proof of design choices in such calculi. The particular design we advocate is illustrated by a multi-focused calculus for full linear logic using an explicitly polarised syntax and incremental focus handling, for which we provide a syntactic cut elimination procedure. We discuss the effect of cut elimination on the structure of proofs, leading to a conceptually simple proof exploiting the strong structure of multi-focused proofs. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1017/S0960129516000451 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
DocType | Volume | Issue |
Journal | 28 | SP5 |
ISSN | Citations | PageRank |
0960-1295 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Taus Brock-Nannestad | 1 | 15 | 4.10 |
| Nicolas Guenot | 2 | 1 | 1.71 |