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)
  Copy   BIBTEX


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.



External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Cut-free Calculi and Relational Semantics for Temporal STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence. Springer. pp. 803 - 819.
The Basics of Display Calculi.Tim Lyon, Christian Ittner, Timo Eckhardt & Norbert Gratzl - 2017 - Kriterion - Journal of Philosophy 31 (2):55-100.
Proof theory for quantified monotone modal logics.Sara Negri & Eugenio Orlandelli - 2019 - Logic Journal of the IGPL 27 (4):478-506.
Maehara-style modal nested calculi.Roman Kuznets & Lutz Straßburger - 2019 - Archive for Mathematical Logic 58 (3-4):359-385.
Gentzen sequent calculi for some intuitionistic modal logics.Zhe Lin & Minghui Ma - 2019 - Logic Journal of the IGPL 27 (4):596-623.
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. Springer. pp. 202-218.
Semantics for a class of intuitionistic modal calculi.Gisele Servi - 1978 - Bulletin of the Section of Logic 7 (1):26-29.
Sufficient conditions for cut elimination with complexity analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1-3):81-99.


Added to PP

243 (#84,413)

6 months
69 (#71,322)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Tim Lyon
Technische Universität Dresden

Citations of this work

Add more citations

References found in this work

The method of hypersequents in the proof theory of propositional non-classical logics.Arnon Avron - 1977 - In Wilfrid Hodges (ed.), Logic. New York: Penguin Books. pp. 1-32.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
Cut-free sequent calculi for some tense logics.Ryo Kashima - 1994 - Studia Logica 53 (1):119 - 135.
Prefixed tableaus and nested sequents.Melvin Fitting - 2012 - Annals of Pure and Applied Logic 163 (3):291 - 313.

View all 15 references / Add more references