Pith. sign in

REVIEW 1 major objections 46 references

Every deep-inference derivation decomposes into an up-fragment followed by a down-fragment whose middle formula is a Lyndon interpolant.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-30 12:03 UTC pith:KMCYRVIJ

load-bearing objection Solid modular deep-inference proof of Lyndon interpolation that also generalizes cut-elim; the only real softness is an unmechanized permutation argument and some modal copy-paste slips. the 1 major comments →

arxiv 2607.23798 v1 pith:KMCYRVIJ submitted 2026-07-26 cs.LO

Interpolation via Generalized Splitting

Lutz Stra{\ss}burger This is my paper
classification cs.LO
keywords proof theorylinear logiccut eliminationinterpolationdeep inferenceLyndon interpolationmodal logicsplitting lemma
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper shows that Lyndon interpolation can be obtained directly inside deep inference, without extracting an interpolant from a sequent proof. The key statement is that any derivation from A to B can be rewritten as a derivation that first uses only “up” rules down to an intermediate formula I and then only “down” rules from I to B. Because up-rules cannot introduce new atoms (or reverse polarity) while moving downward and down-rules cannot do so while moving upward, I automatically satisfies the language and polarity conditions of a Lyndon interpolant. The same decomposition specialises to cut-elimination when the premise is the unit, so interpolation and cut-elimination become two faces of one structural fact. The method is carried out uniformly for linear logic, classical logic and the modal systems K, KT, K4 and S4, for which new cut-free deep-inference calculi are also supplied.

Core claim

Theorem 1 asserts that every derivation A ⊢_X B in the systems considered can be decomposed into A ⊢_{X↑} I ⊢_{X↓} B for some formula I; the intermediate I is necessarily a Lyndon interpolant, and the decomposition simultaneously generalises cut elimination.

What carries the argument

The generalised splitting lemma (Lemma 10) together with the core-flipping lemma: splitting is extended from proofs of (A ⊸ B) ⊸ K to arbitrary-premise derivations, and flipping then turns a mixed up/down derivation into a pure up-then-down derivation while preserving the interpolant.

Load-bearing premise

The whole argument needs a carefully engineered core that contains three extra admissible rules (p′, d′, d′₀ and duals) which are not derivable in the ordinary systems; without that non-standard core the induction for generalised splitting fails.

What would settle it

Exhibit a concrete derivation in one of the listed systems that cannot be rearranged into an up-fragment followed by a down-fragment, or whose forced intermediate formula violates the Lyndon polarity condition.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Interpolation and cut-elimination become instances of a single decomposition theorem rather than separate meta-results.
  • The same core/non-core split immediately yields Lyndon interpolation for classical and the four modal logics once it is proved for linear logic.
  • Novel cut-free deep-inference systems for K, KT, K4 and S4 become available as a by-product.
  • Currying is shown to preserve the up/down decomposition, giving a precise account of how the interpolant transforms under implication introduction.

Where Pith is reading between the lines

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

  • The same modular core/non-core discipline may supply a uniform interpolation criterion for other substructural or modal systems that still lack sequent calculi.
  • Because the decomposition is invertible (up to rule permutation), one obtains a concrete “proof-relevant” interpolant that can be read off atomic flows, linking the result to combinatorial proof theory.
  • Failure of the required core rules for a logic such as K4.3 would give a structural explanation of why that logic lacks interpolation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

1 major / 0 minor

Summary. The paper proposes a deep-inference route to Lyndon interpolation based on a generalized splitting lemma. The main claim, Theorem 1, is that a derivation A ⊢_X B can be decomposed as A ⊢_{X↑} I ⊢_{X↓} B; since down-rules cannot create atoms/polarities going up and up-rules cannot create them going down, I is a Lyndon interpolant, and for A=1 the same statement specializes to cut elimination. The method is developed for linear logic (SLS′), classical logic (SKS), and modal logics K, KT, K4, S4 via new cut-free deep-inference systems. The technical architecture is: generalized splitting for the core fragment (Lemma 10), core flipping (Lemma 12), core/non-core decomposition preserving the ⅋/∨-structure (Lemmas 13, 23, 30), then flipping and interpolation (Theorem 15, Corollary 17, Theorem 31, Corollary 32). Appendices B–E give extensive inductive cases and sequent-calculus simulations.

Significance. If the decomposition lemmas are fully secure, this is a substantial and genuinely modular proof-theoretic contribution: a constructive, syntax-only interpolation proof that strengthens Maehara-style extraction in the direction of Saurin’s proof-relevant interpolation while simultaneously generalizing cut elimination. The core/non-core separation addresses Girard’s modularity complaint in a concrete way, and the transfer from linear to classical and modal logics is elegant. The new cut-free deep-inference systems for K/KT/K4/S4 are independently useful, since deep-inference modal proof theory is underdeveloped. The paper is not machine-checked, but it ships long explicit inductions, stated critical pairs, design rationales for the engineered rules p′↓/d′↓/d′₀↓, and external completeness/cut-elimination anchors; these make the result checkable and falsifiable rather than rhetorical.

major comments (1)
  1. [§4 Lemma 13; Appendix C; Lemmas 23/30] Lemma 13 is the pivot from the core result to Theorem 15 and hence Theorem 1, but the Appendix C proof is still an asserted rule-permutation argument. The displayed critical pairs are persuasive, yet two load-bearing ingredients are missing: (i) an explicit termination measure. The duplication cases for ˚c↓/c↓ replace one core instance below a contraction by two core instances above it, so a naive count of rules or inversions is not obviously well-founded; a lexicographic measure should be stated and shown to decrease in every displayed permutation. (ii) an exhaustiveness argument/table covering all LSnc rules against all LS′c rules, including the quiet cases ai↓, e↓, &↓, ⊤↓, d0↓, ⊗↓ and nested active/passive occurrences, not only the representative critical pairs. Lemmas 23 and 30 inherit this gap by appeal to “same proof.” This is a correctness-risk issue about the permutation proof,不是

Circularity Check

0 steps flagged

No significant circularity: interpolation is constructed by induction on derivations, not assumed or fitted.

full rationale

Theorem 1 and its instances (Corollaries 17, 25, 32) are obtained by an explicit inductive construction: generalized splitting (Lemma 10, induction on derivation size and formula size, all cases written out), core flipping (Lemma 12), core/non-core decomposition by rule permutation (Lemma 13), then flipping (Theorem 15) plus ordinary cut elimination. The interpolant I is produced by the induction; it is not an input, a fitted parameter, or a quantity defined in terms of the target statement. Background facts (soundness/completeness of LS/KS and the modal systems, cut elimination) are standard external theorems, some of which appear in the author’s prior deep-inference papers; those citations supply infrastructure and are not used to smuggle the interpolation claim itself. The engineered core rules p'↓, d'↓, d'₀↓ are openly admitted as extra admissible rules needed for the induction (Remarks 6, 11, 16); that is a design choice, not a definitional loop. No step reduces the claimed decomposition to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 3 invented entities

Load-bearing background is standard proof-theoretic infrastructure (soundness/completeness and cut elimination for linear and classical deep-inference systems; sequent calculi and cut admissibility for K/KT/K4/S4) plus the paper's own engineered rule sets. No free parameters. Invented entities are the new proof systems and the generalized lemmas, which are syntactic constructions with internal proofs rather than physical postulates.

axioms (4)
  • domain assumption Cut elimination / completeness for LS ⊆ X ⊆ SLS' (Theorem 4, Theorem 8) and the corresponding classical facts for KS/SKS
    Used to reduce interpolation to flipping after translating A ⊢ B to a proof of A⊥ ⅋ B and eliminating cut (Corollary 17 steps 1–2). Taken from prior deep-inference literature and sequent translations.
  • domain assumption Sequent systems GS1Y are sound and complete for modal logics Y ∈ {K,KT,K4,S4} with cut admissible (Theorem 40, citing Troelstra–Schwichtenberg, Wansing, Poggiolesi)
    Needed for soundness/completeness and cut elimination of the new deep-inference modal systems via translation (Theorem 27, Corollary 28).
  • standard math De Morgan dualities, multiplicative context lemmas (Lemma 9), and open-deduction derivation formation
    Standard deep-inference and linear-logic infrastructure used throughout splitting and flipping.
  • ad hoc to paper Presence and admissibility of core rules p'↓, d'↓, d'₀↓ (and duals) in LS'c / SLS'c
    Not required for ordinary completeness of linear logic, but required for generalized splitting and O-structure-preserving decomposition (Remarks 6, 11, 14, 16).
invented entities (3)
  • Generalized splitting lemma (Lemma 10) and core flipping lemma (Lemma 12) no independent evidence
    purpose: Extract context splits from derivations with arbitrary premise and flip up/down separation under currying to build the interpolant
    Syntactic lemmas proved by induction; no external referent beyond the proof systems.
  • Deep-inference systems KSY / SKSY for modal logics K, KT, K4, S4 (rules in Figure 3, definition (8)) no independent evidence
    purpose: Provide cut-free deep-inference presentations on which the same interpolation method applies
    New rule sets designed so core/non-core separation and splitting carry over from linear logic via !↔□, ?↔◇.
  • Core/non-core decomposition preserving ⅋/∨ structure (Lemmas 13, 23, 30) no independent evidence
    purpose: Separate non-core structural rules so flipping can be proved on the core then lifted
    Rule-permutation device internal to the method; stronger than prior atomic contraction/weakening decompositions cited.

pith-pipeline@v1.2.0-grok45-kimik3 · 37296 in / 3117 out tokens · 73676 ms · 2026-07-30T12:03:42.181530+00:00 · methodology

0 comments
read the original abstract

We propose a new proof theoretical method for proving Lyndon interpolation. Our proof does not use the sequent calculus but is based on a generalization of the splitting lemma in deep inference. We then formulate the interpolation theorem as a decomposition of a derivation into an up-fragment and a down-fragment. This can be seen as (i) a strengthening of the standard formulation of the interpolation theorem, and (ii) a generalization of the cut elimination theorem. We demonstrate the flexibility of our approach by applying it to linear logic, classical logic, and modal logics. For this, we also introduce novel cut-free proof systems for several modal logics in deep inference.

discussion (0)

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

Reference graph

Works this paper leans on

46 extracted references · 10 canonical work pages · 1 internal anchor

  1. [2]

    Proof Identity and Categorical Models of BV

    Matteo Acclavio, Lutz Stra burger, and Vladimir Zamdzhiev. Proof identity and categorical models of BV . CoRR , abs/2604.25501, 2026. to appear in FSCD 2026. URL: https://doi.org/10.48550/arXiv.2604.25501, https://arxiv.org/abs/2604.25501 arXiv:2604.25501 , https://doi.org/10.48550/ARXIV.2604.25501 doi:10.48550/ARXIV.2604.25501

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2604.25501 2026

  2. [3]

    Removing Cycles from Proofs

    Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs . In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) , volume 82 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 9:1--9:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl -- Leibniz-Zentrum f \"u...

    work page doi:10.4230/lipics.csl.2017.9 2017

  3. [4]

    Interpolation and query rewriting, 2026

    Michael Benedikt. Interpolation and query rewriting, 2026. URL: https://arxiv.org/abs/2606.15737, https://arxiv.org/abs/2606.15737 arXiv:2606.15737

    arXiv 2026

  4. [5]

    Six proofs of interpolation for the modal logic K , 2025

    Nick Bezhanishvili, Balder ten Cate, and Rosalie Iemhoff. Six proofs of interpolation for the modal logic K , 2025. URL: https://arxiv.org/abs/2510.16398, https://arxiv.org/abs/2510.16398 arXiv:2510.16398

    arXiv 2025

  5. [6]

    u nnler. Deep Inference and Symmetry for Classical Proofs . PhD thesis, Tech\-ni\-sche Uni\-ver\-si\-t \

    Kai Br \"u nnler. Deep Inference and Symmetry for Classical Proofs . PhD thesis, Tech\-ni\-sche Uni\-ver\-si\-t \"a t Dres\-den, 2003

    2003

  6. [7]

    Cut elimination inside a deep inference system for classical predicate logic

    Kai Br \"u nnler. Cut elimination inside a deep inference system for classical predicate logic. Studia Logica , 82(1):51--71, 2006

    2006

  7. [8]

    Locality for classical logic

    Kai Br \"u nnler. Locality for classical logic. Notre Dame Journal of Formal Logic , 47(4):557--580, 2006. URL: http://www.iam.unibe.ch/ kai/Papers/LocalityClassical.pdf

    2006

  8. [9]

    A local system for classical logic

    Kai Br \"u nnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors, LPAR 2001 , volume 2250 of LNAI , pages 347--361. Springer, 2001

    2001

  9. [10]

    On the proof complexity of deep inference

    Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic , 10(2):1--34, 2009. Article 14

    2009

  10. [11]

    Splitting and Focusing for Full Propositional Linear Logic in the Calculus of Structures

    Kaustuv Chaudhuri, Nicolas Guenot, Mikheil Rukhaia, and Lutz Strassburger. Splitting and Focusing for Full Propositional Linear Logic in the Calculus of Structures . preprint, 2017. URL: https://inria.hal.science/hal-05493721

    2017

  11. [12]

    The focused calculus of structures

    Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Stra burger. The focused calculus of structures. In Marc Bezem, editor, CSL'11 , volume 12 of LIPIcs , pages 159--173. Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2011

    2011

  12. [13]

    Linear reasoning: A new form of the H erbrand- G entzen theorem

    William Craig. Linear reasoning: A new form of the H erbrand- G entzen theorem. The Journal of Symbolic Logic , 22:250--268, 1957

    1957

  13. [14]

    Three uses of the H erbrand- G entzen theorem in relating model theory and proof theory

    William Craig. Three uses of the H erbrand- G entzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic , 22:269--285, 1957

    1957

  14. [15]

    Modal interpolation via nested sequents

    Melvin Fitting and Roman Kuznets. Modal interpolation via nested sequents. Ann. Pure Appl. Logic , 166(3):274--305, 2015

    2015

  15. [16]

    Linear logic

    Jean-Yves Girard. Linear logic. Theoretical Computer Science , 50:1--102, 1987

    1987

  16. [17]

    Proof Theory and Logical Complexity, Volume I , volume 1 of Studies in Proof Theory

    Jean-Yves Girard. Proof Theory and Logical Complexity, Volume I , volume 1 of Studies in Proof Theory . Bibliopolis, edizioni di filosofia e scienze, 1987

    1987

  17. [18]

    A system of interaction and structure

    Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic , 8(1):1--64, 2007

    2007

  18. [19]

    A Proof Calculus Which Reduces Syntactic Bureaucracy

    Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A Proof Calculus Which Reduces Syntactic Bureaucracy . In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications , volume 6 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 135--150, Dagstuhl, Germany, 2010. Schloss Dagst...

    work page doi:10.4230/lipics.rta.2010.135 2010

  19. [20]

    Non-commutativity and MELL in the calculus of structures

    Alessio Guglielmi and Lutz Stra burger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, Computer Science Logic, CSL 2001 , volume 2142 of LNCS , pages 54--68. Springer-Verlag, 2001

    2001

  20. [21]

    Purity through unravelling

    Robert Hein and Charles Stewart. Purity through unravelling. In Paola Bruscoli, Fran c ois Lamarche, and Charles Stewart, editors, Structures and Deduction , pages 126--143. Technische Universit \"a t Dresden, 2005. ICALP Workshop. ISSN 1430-211X. URL: http://bitschnitzer.de/rh+cas--sd05.pdf

    2005

  21. [22]

    Proofs W ithout S yntax

    Dominic Hughes. Proofs W ithout S yntax. Annals of Mathematics , 164(3):1065--1076, 2006

    2006

  22. [23]

    Towards H ilbert's 24\( ^ th \) problem: Combinatorial proof invariants: (preliminary version)

    Dominic Hughes. Towards H ilbert's 24\( ^ th \) problem: Combinatorial proof invariants: (preliminary version). Electr. Notes Theor. Comput. Sci. , 165:37--63, 2006

    2006

  23. [24]

    Dominic J. D. Hughes, Lutz Stra burger, and Jui - Hsuan Wu. Combinatorial proofs and decomposition theorems for first-order logic. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 , pages 1--13. IEEE , 2021. https://doi.org/10.1109/LICS52264.2021.9470579 doi:10.1109/LICS52264.2021.9470579

    arXiv 2021

  24. [25]

    Interpolation in knowledge representation, 2025

    Jean Christoph Jung, Patrick Koopmann, and Matthias Knorr. Interpolation in knowledge representation, 2025. URL: https://arxiv.org/abs/2512.08833, https://arxiv.org/abs/2512.08833 arXiv:2512.08833

    arXiv 2025

  25. [26]

    From interpolating formulas to separating languages and back again, 2025

    Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. From interpolating formulas to separating languages and back again, 2025. URL: https://arxiv.org/abs/2508.12805, https://arxiv.org/abs/2508.12805 arXiv:2508.12805

    arXiv 2025

  26. [27]

    Interpolation for intermediate logics via injective nested sequents

    Roman Kuznets and Björn Lellmann. Interpolation for intermediate logics via injective nested sequents. Journal of Logic and Computation , 31(3):797--831, 04 2021. https://doi.org/10.1093/logcom/exab015 doi:10.1093/logcom/exab015

    work page doi:10.1093/logcom/exab015 2021

  27. [28]

    Roger C. Lyndon. An interpolation theorem in the predicate calculus. Pacific Journal of Mathematics , 9:129--142, 1959. URL: https://doi.org/10.2140/pjm.1959.9.129

    work page doi:10.2140/pjm.1959.9.129 1959

  28. [29]

    On the interpolation theorem of C raig

    Shoji Maehara. On the interpolation theorem of C raig. S \^u gaku , 12(4), 1960

    1960

  29. [30]

    Maksimova

    L.L. Maksimova. Interpolation theorems in modal logics and amalgamable varieties of topological boolean algebras. Algebra and Logic , 18, 1979. https://doi.org/doi.org/10.1007/BF01673502 doi:doi.org/10.1007/BF01673502

    doi:10.1007/bf01673502 1979

  30. [31]

    Combinatorial flows as bicolored atomic flows

    Giti Omidvar and Lutz Stra burger. Combinatorial flows as bicolored atomic flows. In Agata Ciabattoni, Elaine Pimentel, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022, Ia s i, Romania, September 20-23, 2022, Proceedings , volume 13468 of Lecture Notes in Computer Science , pag...

    work page doi:10.1007/978-3-031-15298-6 2022

  31. [32]

    Gentzen Calculi for Modal Propositional Logic

    Francesca Poggiolesi. Gentzen Calculi for Modal Propositional Logic . Springer, 2011. https://doi.org/doi.org/10.1007/978-90-481-9670-8 doi:doi.org/10.1007/978-90-481-9670-8

    work page doi:10.1007/978-90-481-9670-8 2011

  32. [33]

    Modular Normalisation of Classical Proofs

    Benjamin Ralph. Modular Normalisation of Classical Proofs . PhD thesis, University of Bath, 2019

    2019

  33. [34]

    Towards a combinatorial proof theory

    Benjamin Ralph and Lutz Stra burger. Towards a combinatorial proof theory. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings , volume 11714 of Lecture Notes in Computer Science , pages 259--276. Spring...

    work page doi:10.1007/978-3-030-29026-9 2019

  34. [35]

    Interpolation in fragments of classical linear logic

    Dirk Roorda. Interpolation in fragments of classical linear logic. Journal of Symbolic Logic , 59(2):419--444, 1994. https://doi.org/10.2307/2275398 doi:10.2307/2275398

    work page doi:10.2307/2275398 1994

  35. [36]

    Craig interpolation in program verification, 2026

    Philipp Rümmer. Craig interpolation in program verification, 2026. URL: https://arxiv.org/abs/2602.08532, https://arxiv.org/abs/2602.08532 arXiv:2602.08532

    arXiv 2026

  36. [37]

    Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation

    Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation . In Maribel Fern\' a ndez, editor, 10th International Conference on Formal Structures for Computation and Deduction ( FSCD 2025) , volume 337 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 32:1--32:21, Dagstuhl, Germany, 2025...

    doi:10.4230/lipics.fscd.2025.32 2025

  37. [38]

    A systematic proof theory for several modal logics

    Charles Stewart and Phiniki Stouppa. A systematic proof theory for several modal logics. In R. A. Schmidt, I. Pratt-Hartmann, M. Reynolds, and H. Wansing, editors, Advances in Modal Logic, Volume 5 , pages 309--333. King's College Publications, 2005

    2005

  38. [39]

    A local system for linear logic

    Lutz Stra burger . A local system for linear logic. In Matthias Baaz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002 , volume 2514 of LNAI , pages 388--402. Springer-Verlag, 2002. URL: http://www.lix.polytechnique.fr/ lutz/papers/LocSysLinLog.pdf

    2002

  39. [40]

    Linear Logic and Noncommutativity in the Calculus of Structures

    Lutz Stra burger. Linear Logic and Noncommutativity in the Calculus of Structures . PhD thesis, Tech\-ni\-sche Uni\-ver\-si\-t \"a t Dres\-den, 2003

    2003

  40. [41]

    MELL in the C alculus of S tructures

    Lutz Stra burger. MELL in the C alculus of S tructures. Theoretical Computer Science , 309(1--3):213--285, 2003

    2003

  41. [42]

    Combinatorial flows and their normalisation

    Lutz Stra burger. Combinatorial flows and their normalisation. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK , volume 84 of LIPIcs , pages 31:1--31:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017

    2017

  42. [43]

    A system of interaction and structure IV : The exponentials and decomposition

    Lutz Stra burger and Alessio Guglielmi. A system of interaction and structure IV : The exponentials and decomposition. ACM Trans. Comput. Log. , 12(4):23, 2011

    2011

  43. [44]

    Basic Proof Theory

    Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory . Cambridge University Press, second edition, 2000

    2000

  44. [45]

    Introduction to deep inference

    Andrea Aler Tubella and Lutz Stra burger. Introduction to deep inference. Lecture notes for ESSLLI'19, 2019. URL: https://hal.inria.fr/hal-02390267

    2019

  45. [46]

    Interpolation in proof theory, 2026

    Iris van der Giessen, Raheleh Jalali, and Roman Kuznets. Interpolation in proof theory, 2026. URL: https://arxiv.org/abs/2602.16318, https://arxiv.org/abs/2602.16318 arXiv:2602.16318

    arXiv 2026

  46. [47]

    Sequent systems for modal logics

    Heinrich Wansing. Sequent systems for modal logics. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic: Volume 8 , pages 61--145. Springer Netherlands, Dordrecht, 2002. https://doi.org/10.1007/978-94-010-0387-2_2 doi:10.1007/978-94-010-0387-2_2

    work page doi:10.1007/978-94-010-0387-2_2 2002