pith. sign in

arxiv: 2511.22174 · v2 · submitted 2025-11-27 · 💻 cs.LO · math.LO

Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability

Tim S. Lyon This is my paper

Pith reviewed 2026-05-17 05:12 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords intuitionistic modal logicnested sequentsgrammar logicscut-eliminationundecidabilitynegative translationmulti-modal logicstense logics
0
0 comments X

The pith

A faithful negative translation embeds classical grammar logics into intuitionistic ones, establishing undecidability of the validity problem for intuitionistic grammar logics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs single-conclusion nested sequent calculi for intuitionistic grammar logics, which generalize standard intuitionistic modal and tense logics with combinations of T, B, 4, 5, and D axioms. It introduces a shift rule that consolidates various structural rules for frame conditions, supporting uniform proofs of invertibility, admissibility, and cut-elimination across the entire class. The central result is a negative translation that faithfully embeds classical grammar logics into these intuitionistic systems via proof transformations, reducing the known undecidable validity problem for classical cases to the intuitionistic setting.

Core claim

By defining a negative translation from classical grammar logics to intuitionistic grammar logics and verifying faithfulness through mappings between multi-conclusion and single-conclusion nested sequent proofs, the authors reduce the general validity problem for classical grammar logics to that for intuitionistic grammar logics, implying undecidability for the latter since it is already undecidable for the former.

What carries the argument

The shift rule, a novel structural rule that unifies frame-condition rules for T, B, 4, 5, and D into one, enabling a uniform syntactic cut-admissibility proof over all intuitionistic grammar logics.

If this is right

  • The nested sequent calculi are cut-free and complete for every intuitionistic grammar logic in the class.
  • A single uniform procedure decides cut-admissibility without separate proofs for each axiom combination.
  • Validity checking in any intuitionistic grammar logic reduces directly to the corresponding classical case.
  • Standard intuitionistic modal logics such as IK and IKt with added axioms inherit the undecidability result.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar negative translations could transfer decidability or complexity results between classical and intuitionistic variants of other modal logics.
  • The modular shift rule might simplify implementation of automated theorem provers for families of intuitionistic modal systems.
  • The embedding technique suggests that proof-search complexity in intuitionistic grammar logics tracks that of their classical counterparts.

Load-bearing premise

The negative translation preserves validity for every combination of the T, B, 4, 5, and D axioms while the shift rule correctly captures all corresponding frame conditions.

What would settle it

A concrete counterexample formula that is valid in some intuitionistic grammar logic but whose image under the negative translation is not valid in the corresponding classical grammar logic, or vice versa.

Figures

Figures reproduced from arXiv: 2511.22174 by Tim S. Lyon.

Figure 1
Figure 1. Figure 1: Depictions of the (F1) and (F2) conditions imposed on models. Dotted arrows [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The nested sequent system NIKm(A) defined relative to the set A of axioms. Note that dx ∈ NIKm(A) iff Dx ∈ A. We sometimes refer to a component as a w-component if w is the name of that com￾ponent, and we use the notation G{H1}w1 . . . {Hn}wn to indicate that Hi is ‘rooted at’ the wi-component of G for i ∈ [n]. Often, we will more simply write G{H1} . . . {Hn} if the names of the components are not of rele… view at source ↗
Figure 3
Figure 3. Figure 3: A diagram depicting which hp-admissibility (and hp-invertibility) results are suf [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Height-preserving admissible rules in NIKm(A). The remaining hp-admissibility results are all proven by induction on the height of the given proof π. Lemma 4.2. The ⊥R, necx, wL, wR, and ew rules are hp-admissible in NIKm(A). Proof. Let r ∈ {⊥R, necx, wL,wR, ew}. We make a case distinction on the last rule r ′ ∈ NIKm(A) applied in the given proof π. Observe that applying r (if possible) to an id or ⊥L inst… view at source ↗
Figure 5
Figure 5. Figure 5: Some interpolation rules. (1) sig◦ (I ⇒ J ) = sig• (I) ∪ sig◦ (J ); (2) sig◦ (I ⊕ J ) = sig◦ (I) ∪ sig◦ (J ) for ⊕ ∈ { , }; (3) sig◦ (∇xI) = sig◦ (I) for ∇x ∈ {⟨x⟩, [x]}. Lemma 5.4. If NIKm(A), π ⊩ G, then for any biasing Ge of G there exists an interpolation proof π ′ and interpolant I such that NIKI m(A), π′ ⊩ G ∥ I e and (1) Names(I) ⊆ Names(Ge); (2) sig◦ (I) ⊆ sig• (GeL ) ∩ sig◦ (GeR ). 27 [PITH_FULL_… view at source ↗
read the original abstract

We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical grammar logics, and subsume standard intuitionistic modal and tense logics, including IK and IKt extended with combinations of the T, B, 4, 5, and D axioms. We analyze fundamental invertibility and admissibility properties of our calculi and introduce a novel structural rule, called the "shift rule," which unifies standard structural rules arising from modal frame conditions into a single rule. This rule enables a purely syntactic proof of cut-admissibility that is uniform over all IGLs, and yields completeness of our nested calculi as a corollary. Finally, we define a negative translation that constitutes a faithful embedding of classical grammar logics (CGLs) into IGLs, witnessed by proof transformations between multi-conclusioned and single-conclusioned nested sequent proofs for CGLs and IGLs, respectively. This reduces the general validity problem for CGLs to that of IGLs. The general validity problem over a class C of logics asks: given a logic L in C and a formula A, is A valid in L? As this problem is known to be undecidable for CGLs, our reduction implies its undecidability for IGLs as well.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces single-conclusion nested sequent calculi for intuitionistic grammar logics (IGLs), which extend standard intuitionistic modal logics with arbitrary combinations of the T, B, 4, 5, and D axioms. It defines a novel shift rule that unifies structural rules arising from modal frame conditions, establishes invertibility and admissibility properties, and gives a uniform syntactic proof of cut-admissibility that yields completeness. It further defines a negative translation that embeds classical grammar logics (CGLs) into IGLs via proof transformations between multi-conclusion and single-conclusion nested sequents, reducing the known undecidability of the general validity problem for CGLs to IGLs.

Significance. If the central results hold, the work supplies a modular, uniform proof-theoretic framework for a wide family of intuitionistic multi-modal logics together with a syntactic cut-elimination argument that applies across all IGLs. The negative-translation embedding is a technically interesting bridge between classical and intuitionistic grammar logics and directly yields undecidability of the general validity problem for IGLs, a result that strengthens the landscape of decidability/undecidability results in non-classical modal logic.

major comments (2)
  1. [Negative translation and embedding (Section on negative translation)] The faithfulness claim for the negative translation (witnessed by proof transformations) is load-bearing for the undecidability reduction. The abstract states that the translation preserves validity for every combination of T, B, 4, 5, and D, yet the interaction of D (seriality) and 5 (Euclidean) with the intuitionistic preorder, modal accessibility relation, and persistence condition is non-trivial; an explicit verification or case analysis for all 2^5 combinations, especially D+5, is required to confirm that the embedding is faithful in both directions.
  2. [Definition and properties of the shift rule] The shift rule is presented as correctly encoding all frame conditions for the entire class of IGLs and enabling the uniform cut-elimination argument. Because the rule is the key device that replaces the usual collection of structural rules, the manuscript must demonstrate that the rule is sound and complete with respect to the full set of frame conditions for every combination, including those involving D and 5; otherwise the uniformity claim and the subsequent completeness corollary rest on an unverified assumption.
minor comments (2)
  1. [Preliminaries] Notation for the two accessibility relations (intuitionistic preorder and modal accessibility) should be introduced with explicit persistence clauses at the first use to avoid ambiguity when discussing mixed axiom sets.
  2. [Abstract] The abstract would benefit from a short concrete example illustrating how the shift rule replaces two or three standard structural rules for a specific axiom combination such as 4+5.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report, and for the positive assessment of the significance of our results. We address each major comment below and indicate the revisions we will undertake.

read point-by-point responses

  1. Referee: [Negative translation and embedding (Section on negative translation)] The faithfulness claim for the negative translation (witnessed by proof transformations) is load-bearing for the undecidability reduction. The abstract states that the translation preserves validity for every combination of T, B, 4, 5, and D, yet the interaction of D (seriality) and 5 (Euclidean) with the intuitionistic preorder, modal accessibility relation, and persistence condition is non-trivial; an explicit verification or case analysis for all 2^5 combinations, especially D+5, is required to confirm that the embedding is faithful in both directions.

    Authors: We agree that making the faithfulness verification fully explicit strengthens the presentation. The manuscript already contains a general semantic argument establishing that the negative translation preserves validity for arbitrary combinations of the axioms, relying on the correspondence between the single-conclusion nested sequent rules and the frame conditions together with the proof transformations between multi- and single-conclusion systems. To address the referee's request directly, the revised version will include an appendix with a compact case analysis covering all 32 combinations. The analysis for D+5 will explicitly check the interaction with the intuitionistic preorder and persistence condition, confirming both directions of the embedding. This addition does not alter the existing general proof but renders the verification fully transparent. revision: yes

  2. Referee: [Definition and properties of the shift rule] The shift rule is presented as correctly encoding all frame conditions for the entire class of IGLs and enabling the uniform cut-elimination argument. Because the rule is the key device that replaces the usual collection of structural rules, the manuscript must demonstrate that the rule is sound and complete with respect to the full set of frame conditions for every combination, including those involving D and 5; otherwise the uniformity claim and the subsequent completeness corollary rest on an unverified assumption.

    Authors: The shift rule is defined so that its instances directly correspond to the modal frame conditions induced by any subset of {T, B, 4, 5, D}. Soundness and completeness of the rule (relative to the class of frames satisfying the selected conditions) are established in the manuscript by a uniform semantic argument that does not depend on the particular combination chosen. Nevertheless, we acknowledge the value of making the encoding explicit for the non-standard cases. The revised manuscript will add a short subsection that spells out how the shift rule encodes seriality (D) and the Euclidean property (5) in the presence of the intuitionistic preorder and persistence, thereby confirming that the uniformity claim holds for these combinations as well. revision: yes

Circularity Check

0 steps flagged

No circularity: syntactic cut-elimination and external reduction to known CGL undecidability

full rationale

The paper defines single-conclusion nested sequent calculi for IGLs, introduces the shift rule as a novel unification of structural rules, proves cut-admissibility syntactically and uniformly, and obtains completeness as a corollary. It then defines a negative translation and establishes faithfulness via explicit proof transformations between multi- and single-conclusion nested sequent systems. Undecidability of IGL validity follows directly from the known undecidability for CGLs via this embedding. None of these steps reduce by construction to prior inputs, self-definitions, or unverified self-citations; the embedding and transformations supply independent syntactic content, and the CGL undecidability is treated as an external known result.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The work rests on standard sequent-calculus axioms and modal frame conditions; the main addition is the shift rule as a new structural construct rather than new logical axioms or fitted parameters.

axioms (1)
  • domain assumption Standard invertibility and admissibility properties of nested sequents hold for the base intuitionistic modal logic IK and its extensions
    Invoked to support the uniform treatment of IGLs that subsume IK and IKt plus T, B, 4, 5, D.
invented entities (1)
  • shift rule no independent evidence
    purpose: Unifies multiple structural rules arising from modal frame conditions into one rule
    Introduced to obtain a single syntactic cut-admissibility proof that works for the entire class of IGLs.

pith-pipeline@v0.9.0 · 5567 in / 1325 out tokens · 42830 ms · 2026-05-17T05:12:23.153403+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

59 extracted references · 59 canonical work pages · 1 internal anchor

  1. [1]

    Cambridge University Press, 2017

    Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler.Introduction to Description Logic. Cambridge University Press, 2017

    work page 2017

  2. [2]

    Display logic.Journal of Philosophical Logic, 11(4):375–417, 1982

    Nuel D Belnap. Display logic.Journal of Philosophical Logic, 11(4):375–417, 1982

    work page 1982

  3. [3]

    On padoa’s method in the theory of definition.Journal of Symbolic Logic, 21(2):194–195, 1956

    Evert Willem Beth. On padoa’s method in the theory of definition.Journal of Symbolic Logic, 21(2):194–195, 1956

    work page 1956

  4. [4]

    Models for normal intuitionistic modal logics.Studia Logica, 43(3):217–245, 1984

    Milan Boˇ zi´ c and Kosta Doˇ sen. Models for normal intuitionistic modal logics.Studia Logica, 43(3):217–245, 1984

    work page 1984

  5. [5]

    Deep sequent systems for modal logic.Archive for Math- ematical Logic, 48(6):551–577, 2009

    Kai Br¨ unnler. Deep sequent systems for modal logic.Archive for Math- ematical Logic, 48(6):551–577, 2009. doi: 10.1007/s00153-009-0137-3. URL https://doi.org/10.1007/s00153-009-0137-3

    work page doi:10.1007/s00153-009-0137-3 2009

  6. [6]

    Robert A. Bull. A modal extension of intuitionist logic.Notre Dame Journal of Formal Logic, 6(2):142, 1965

    work page 1965

  7. [7]

    Robert A. Bull. Cut elimination for propositional dynamic logic without *.Zeitschrift f¨ ur Mathematische Logik und Grundlagen der Mathematik, 38(2):85–100, 1992

    work page 1992

  8. [8]

    An introduction to proof theory.Handbook of proof theory, 137:1–78, 1998

    Samuel R Buss. An introduction to proof theory.Handbook of proof theory, 137:1–78, 1998

    work page 1998

  9. [9]

    Display to la- belled proofs and back again for tense logics.ACM Transactions on Computational Logic, 22(3):1–31, 2021

    Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to la- belled proofs and back again for tense logics.ACM Transactions on Computational Logic, 22(3):1–31, 2021

    work page 2021

  10. [10]

    Three uses of the herbrand-gentzen theorem in relating model theory and proof theory.Journal of Symbolic Logic, 22(3):269–285, 1957

    William Craig. Three uses of the herbrand-gentzen theorem in relating model theory and proof theory.Journal of Symbolic Logic, 22(3):269–285, 1957. doi: 10.2307/2963594

    work page doi:10.2307/2963594 1957

  11. [11]

    A modal analysis of staged computation.Journal of the ACM, 48(3):555–604, May 2001

    Rowan Davies and Frank Pfenning. A modal analysis of staged computation.Journal of the ACM, 48(3):555–604, May 2001. ISSN 0004-5411

    work page 2001

  12. [12]

    Deciding regular grammar logics with converse through first-order logic.Journal of Logic, Language and Information, 14(3):289–329, 2005

    St´ ephane Demri and Hans de Nivelle. Deciding regular grammar logics with converse through first-order logic.Journal of Logic, Language and Information, 14(3):289–329, 2005

    work page 2005

  13. [13]

    Models for stronger normal intuitionistic modal logics.Studia Logica, 44 (1):39–70, 1985

    Kosta Doˇ sen. Models for stronger normal intuitionistic modal logics.Studia Logica, 44 (1):39–70, 1985

    work page 1985

  14. [14]

    Contraction-free sequent calculi for intuitionistic logic.The Journal of Symbolic Logic, 57(3):795–807, 1992

    Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic.The Journal of Symbolic Logic, 57(3):795–807, 1992

    work page 1992

  15. [15]

    W. B. Ewald. Intuitionistic tense and modal logic.The Journal of Symbolic Logic, 51 (1):166–179, 1986. ISSN 00224812. 33

    work page 1986

  16. [16]

    An intuitionistic modal logic with applications to the formal verification of hardware

    Matt Fairtlough and Michael Mendler. An intuitionistic modal logic with applications to the formal verification of hardware. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, pages 354–368, Berlin, Heidelberg, 1995. Springer Berlin Hei- delberg. ISBN 978-3-540-49404-1

    work page 1995

  17. [17]

    Axiomatizations for some intuitionistic modal logics.Rendiconti del Seminario Matematico Universit` a e Politecnico di Torino, 42(3):179–194, 1984

    G Fischer-Servi. Axiomatizations for some intuitionistic modal logics.Rendiconti del Seminario Matematico Universit` a e Politecnico di Torino, 42(3):179–194, 1984

    work page 1984

  18. [18]

    On modal logic with an intuitionistic base.Stu- dia Logica, 36(3):141–149, 1977

    Gis` ele Fischer Servi. On modal logic with an intuitionistic base.Stu- dia Logica, 36(3):141–149, 1977. doi: 10.1007/BF02121259. URL https://doi.org/10.1007/BF02121259

    work page doi:10.1007/bf02121259 1977

  19. [19]

    Frederic B. Fitch. Intuitionistic modal logic with quantifiers.Portugaliae mathematica, 7(2):113–118, 1948

    work page 1948

  20. [20]

    Modal interpolation via nested sequents.Annals of Pure and Applied Logic, 166(3):274–305, 2015

    Melvin Fitting and Roman Kuznets. Modal interpolation via nested sequents.Annals of Pure and Applied Logic, 166(3):274–305, 2015

    work page 2015

  21. [21]

    Untersuchungen ¨ uber das logische Schließen

    Gerhard Gentzen. Untersuchungen ¨ uber das logische Schließen. i.Mathematische zeitschrift, 39(1):176–210, 1935

    work page 1935

  22. [22]

    Untersuchungen ¨ uber das logische Schließen

    Gerhard Gentzen. Untersuchungen ¨ uber das logische Schließen. ii.Mathematische Zeitschrift, 39(1):405–431, 1935

    work page 1935

  23. [23]

    Model theory of modal logic

    Valentin Goranko and Martin Otto. Model theory of modal logic. In Patrick Blackburn, Johan Van Benthem, and Frank Wolter, editors,Handbook of Modal Logic, volume 3 ofStudies in Logic and Practical Reasoning, pages 249–

    work page

  24. [24]

    doi: https://doi.org/10.1016/S1570-2464(07)80008-5

    Elsevier, 2007. doi: https://doi.org/10.1016/S1570-2464(07)80008-5. URL https://www.sciencedirect.com/science/article/pii/S1570246407800085

    work page doi:10.1016/s1570-2464(07)80008-5 2007

  25. [25]

    On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.Logical Methods in Computer Science, 7(2), 2011

    Rajeev Gor´ e, Linda Postniece, and Alwen Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.Logical Methods in Computer Science, 7(2), 2011

    work page 2011

  26. [26]

    An Intuitionisticaly based Description Logic

    Edward Hermann Haeusler and Alexandre Rademaker. An intuitionisticaly based de- scription logic, 2014. URLhttps://arxiv.org/abs/1402.0225

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  27. [27]

    Intuitionistic description logic and legal reasoning

    Edward Hermann Haeusler, Valeria de Paiva, and Alexandre Rademaker. Intuitionistic description logic and legal reasoning. In2011 22nd International Workshop on Database and Expert Systems Applications, pages 345–349, 2011. doi: 10.1109/DEXA.2011.46

    work page doi:10.1109/dexa.2011.46 2011

  28. [28]

    Decidability of shiq with complex role inclusion axioms

    Ian Horrocks and Ulrike Sattler. Decidability of shiq with complex role inclusion axioms. Artificial Intelligence, 160(1-2):79–104, 2004

    work page 2004

  29. [29]

    On enumerating query plans using analytic tableau

    Alexander Hudek, David Toman, and Grant Weddell. On enumerating query plans using analytic tableau. In Hans De Nivelle, editor,Automated Reasoning with Ana- lytic Tableaux and Related Methods, pages 339–354, Cham, 2015. Springer International Publishing. ISBN 978-3-319-24312-2. 34

    work page 2015

  30. [30]

    Tree-sequent methods for subintuitionistic predicate logics

    Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor,Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 ofLecture Notes in Computer Science, pages 149–164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. ISBN 978-3-540-73099-6

    work page 2007

  31. [31]

    Cut-free sequent calculi for some tense logics.Studia Logica, 53(1): 119–135, 1994

    Ryo Kashima. Cut-free sequent calculi for some tense logics.Studia Logica, 53(1): 119–135, 1994

    work page 1994

  32. [32]

    Multicomponent proof-theoretic method for proving interpolation properties.Annals of Pure and Applied Logic, 169(12):1369–1418, 2018

    Roman Kuznets. Multicomponent proof-theoretic method for proving interpolation properties.Annals of Pure and Applied Logic, 169(12):1369–1418, 2018

    work page 2018

  33. [33]

    Maehara-style modal nested calculi.Archive for Mathematical Logic, 58(3):359–385, 2019

    Roman Kuznets and Lutz Straßburger. Maehara-style modal nested calculi.Archive for Mathematical Logic, 58(3):359–385, 2019. doi: 10.1007/s00153-018-0636-1. URL https://doi.org/10.1007/s00153-018-0636-1

    work page doi:10.1007/s00153-018-0636-1 2019

  34. [34]

    Proof theoretic methodology for propositional dynamic logic

    Daniel Leivant. Proof theoretic methodology for propositional dynamic logic. In J. D´ ıaz and I. Ramos, editors,Formalization of Programming Concepts, pages 356–373, Berlin, Heidelberg, 1981. Springer. ISBN 978-3-540-38654-4

    work page 1981

  35. [35]

    Springer International Publishing, Cham, 2024

    Bj¨ orn Lellmann and Francesca Poggiolesi.Nested Sequents or Tree-Hypersequents—A Survey, pages 243–301. Springer International Publishing, Cham, 2024. ISBN 978-3- 031-57635-5. doi: 10.1007/978-3-031-57635-5 11

    work page doi:10.1007/978-3-031-57635-5 2024

  36. [36]

    Roger C. Lyndon. An Interpolation Theorem in the Predicate Calculus.Pacific Journal of Mathematics, 9(1):129 – 142, 1959

    work page 1959

  37. [37]

    On deriving nested calculi for intuitionistic logics from semantic sys- tems

    Tim Lyon. On deriving nested calculi for intuitionistic logics from semantic sys- tems. In Sergei N. Art¨ emov and Anil Nerode, editors,Logical Foundations of Computer Science, Proceedings, volume 11972 ofLecture Notes in Computer Sci- ence, pages 177–194. Springer, 2020. doi: 10.1007/978-3-030-36755-8 12. URL https://doi.org/10.1007/978-3-030-36755-8 12

    work page doi:10.1007/978-3-030-36755-8 2020

  38. [38]

    PhD thesis, Technische Universit¨ at Wien, 2021

    Tim Lyon.Refining Labelled Systems for Modal and Constructive Logics with Applica- tions. PhD thesis, Technische Universit¨ at Wien, 2021

    work page 2021

  39. [39]

    Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents

    Tim Lyon, Alwen Tiu, Rajeev Gor´ e, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fern´ andez and Anca Muscholl, editors,28th EACSL Annual Conference on Computer Science Logic, volume 152 ofLIPIcs, pages 28:1–28:16. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2020

    work page 2020

  40. [40]

    Tim S. Lyon. Nested sequents for intuitionistic modal logics via structural refinement. In Anupam Das and Sara Negri, editors,Automated Reasoning with Analytic Tableaux and Related Methods, pages 409–427, Cham, 2021. Springer International Publishing. ISBN 978-3-030-86059-2

    work page 2021

  41. [41]

    Tim S. Lyon. A framework for intuitionistic grammar logics. In Pietro Baroni, Christoph Benzm¨ uller, and Y` ı N. W´ ang, editors,Logic and Argumentation, pages 495–503, Cham,

    work page

  42. [42]

    ISBN 978-3-030-89391-0

    Springer International Publishing. ISBN 978-3-030-89391-0. 35

    work page

  43. [43]

    Lyon and Luc´ ıa G´ omez´Alvarez

    Tim S. Lyon and Luc´ ıa G´ omez´Alvarez. Automating reasoning with standpoint logic via nested sequents. InProceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, pages 257–266, 8 2022

    work page 2022

  44. [44]

    Lyon and Jonas Karge

    Tim S. Lyon and Jonas Karge. Constructive interpolation and concept-based beth definability for description logics via sequents. InProceedings of the Thirty-Third Inter- national Joint Conference on Artificial Intelligence (IJCAI), pages 3484–3492. ijcai.org,

    work page

  45. [45]

    URLhttps://www.ijcai.org/proceedings/2024/386

    work page 2024

  46. [46]

    J., 2022, in Bambi C., Santangelo A., eds, , Handbook of X-ray and Gamma-ray Astrophysics

    Tim S. Lyon and Eugenio Orlandelli. Nested sequents for quantified modal logics. InAutomated Reasoning with Analytic Tableaux and Related Methods, page 449–467, Berlin, Heidelberg, 2023. Springer-Verlag. ISBN 978-3-031-43512-6. doi: 10.1007/978- 3-031-43513-3 24

    work page doi:10.1007/978- 2023

  47. [47]

    Lyon and Piotr Ostropolski-Nalewaja

    Tim S. Lyon and Piotr Ostropolski-Nalewaja. Foundations for an abstract proof theory in the context of Horn rules, 2023. URLhttps://arxiv.org/abs/2304.05697

    work page arXiv 2023

  48. [48]

    On the interpolation theorem of Craig.Sˆ ugaku, 12(4):235–237, 1960

    Shoji Maehara. On the interpolation theorem of Craig.Sˆ ugaku, 12(4):235–237, 1960

    work page 1960

  49. [49]

    A fully labelled proof system for intuitionistic modal logics.Journal of Logic and Computation, 31 (3):998–1022, 05 2021

    Sonia Marin, Marianela Morales, and Lutz Straßburger. A fully labelled proof system for intuitionistic modal logics.Journal of Logic and Computation, 31 (3):998–1022, 05 2021. ISSN 0955-792X. doi: 10.1093/logcom/exab020. URL https://doi.org/10.1093/logcom/exab020

    work page doi:10.1093/logcom/exab020 2021

  50. [50]

    (eds.): Handbook of Model Checking

    Kenneth L. McMillan. Interpolation and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors,Handbook of Model Checking, pages 421–446. Springer International Publishing, Cham, 2018. ISBN 978-3- 319-10575-8. doi: 10.1007/978-3-319-10575-8 14

    work page doi:10.1007/978-3-319-10575-8 2018

  51. [51]

    Evaluation logic

    Andrew M Pitts. Evaluation logic. InIV Higher Order Workshop, pages 162–189. Springer, 1991

    work page 1991

  52. [52]

    A framework for intuitionistic modal logics: Ex- tended abstract

    Gordon Plotkin and Colin Stirling. A framework for intuitionistic modal logics: Ex- tended abstract. InProceedings of Theoretical Aspects of Reasoning about Knowledge, TARK ’86, page 399–406, San Francisco, CA, USA, 1986. Morgan Kaufmann Publishers Inc. ISBN 0934613049

    work page 1986

  53. [53]

    The method of tree-hypersequents for modal proposi- tional logic

    Francesca Poggiolesi. The method of tree-hypersequents for modal proposi- tional logic. In David Makinson, Jacek Malinowski, and Heinrich Wans- ing, editors,Towards Mathematical Philosophy, volume 28 ofTrends in logic, pages 31–51. Springer, 2009. doi: 10.1007/978-1-4020-9084-4 3. URL https://doi.org/10.1007/978-1-4020-9084-4 3

    work page doi:10.1007/978-1-4020-9084-4 2009

  54. [54]

    Recursive unsolvability of a problem of Thue.The Journal of Symbolic Logic, 12(1):1–11, 1947

    Emil L Post. Recursive unsolvability of a problem of Thue.The Journal of Symbolic Logic, 12(1):1–11, 1947

    work page 1947

  55. [55]

    PhD the- sis, University of Edinburgh

    Alex K Simpson.The proof theory and semantics of intuitionistic modal logic. PhD the- sis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994. 36

    work page 1994

  56. [56]

    Intuitionistic modal logic: A 15-year retrospective.Journal of Logic and Computation, 28(5): 873–882, 06 2015

    Charles Stewart, Valeria de Paiva, and Natasha Alechina. Intuitionistic modal logic: A 15-year retrospective.Journal of Logic and Computation, 28(5): 873–882, 06 2015. ISSN 0955-792X. doi: 10.1093/logcom/exv042. URL https://doi.org/10.1093/logcom/exv042

    work page doi:10.1093/logcom/exv042 2015

  57. [57]

    Cut elimination in nested sequents for intuitionistic modal logics

    Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Frank Pfenning, editor,Foundations of Software Science and Computation Structures, volume 7794 ofLecture Notes in Computer Science, pages 209–224, Berlin, Heidelberg,

    work page

  58. [58]

    ISBN 978-3-642-37075-5

    Springer Berlin Heidelberg. ISBN 978-3-642-37075-5

    work page

  59. [59]

    Grammar logics in nested sequent calculus: Proof theory and decision procedures

    Alwen Tiu, Egor Ianovski, and Rajeev Gor´ e. Grammar logics in nested sequent calculus: Proof theory and decision procedures. In Thomas Bolander, Torben Bra¨ uner, Silvio Ghilardi, and Lawrence S. Moss, editors,Advances in Modal Logic 9, pages 516–537. College Publications, 2012. 37

    work page 2012