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
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.
(categorize this paper)
PhilPapers/Archive ID
Upload history
Archival date: 2020-02-03
View other versions
Added to PP index

Total views
75 ( #50,398 of 2,454,523 )

Recent downloads (6 months)
9 ( #49,968 of 2,454,523 )

How can I increase my downloads?

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