On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelLogical Foundations of Computer Science
Redakteure/-innenSergei Artemov, Anil Nerode
ErscheinungsortCham
Herausgeber (Verlag)Springer International Publishing AG
Seiten177-194
Seitenumfang18
ISBN (Print)978-3-030-36755-8
PublikationsstatusVeröffentlicht - 2020
Peer-Review-StatusJa

Externe IDs

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