On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

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 languageEnglish
Title of host publicationLogical Foundations of Computer Science
EditorsSergei Artemov, Anil Nerode
Place of PublicationCham
PublisherSpringer International Publishing AG
Pages177-194
Number of pages18
ISBN (print)978-3-030-36755-8
Publication statusPublished - 2020
Peer-reviewedYes

External IDs

Scopus 85077499091
ORCID /0000-0003-3214-0828/work/142249493