On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science. Cham: pp. 177-194 (2020)
Download Edit this record How to cite View on PhilPapers
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.
Categories
(categorize this paper)
PhilPapers/Archive ID
LYOODN
Upload history
Archival date: 2020-02-03
View other versions
Added to PP index
2019-12-26

Total views
35 ( #48,203 of 52,923 )

Recent downloads (6 months)
20 ( #30,108 of 52,923 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.