On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated labelled calculus.
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 | 177-194 |
Number of pages | 18 |
ISBN (print) | 978-3-030-36755-8 |
Publication status | Published - 2020 |
Peer-reviewed | Yes |
External IDs
Scopus | 85077499091 |
---|---|
ORCID | /0000-0003-3214-0828/work/142249493 |