From Display to Labelled Proofs for Tense Logics
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.
Details
| Original language | English |
|---|---|
| Title of host publication | Logical Foundations of Computer Science |
| Editors | Sergei Artemov, Anil Nerode |
| Place of Publication | Cham |
| Publisher | Springer International Publishing AG |
| Pages | 120-139 |
| Number of pages | 20 |
| ISBN (print) | 978-3-319-72056-2 |
| Publication status | Published - 2018 |
| Peer-reviewed | Yes |
External IDs
| Scopus | 85039457502 |
|---|---|
| ORCID | /0000-0003-3214-0828/work/142249480 |