Craig Interpolation in Displayable Logics
From MaRDI portal
Publication:3010362
DOI10.1007/978-3-642-22119-4_9zbMath1333.03107OpenAlexW66773879MaRDI QIDQ3010362
James Brotherston, Rajeev Goré
Publication date: 1 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1885/36361
Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Interpolation, preservation, definability (03C40)
Related Items
Craig Interpolation in Displayable Logics ⋮ Hypersequent and display calculi -- a unified perspective ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi ⋮ Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
Cites Work
- Unnamed Item
- Unnamed Item
- Failure of interpolation in relevant logics
- Harmonious logic: Craig's interpolation theorem and its descendants
- Handbook of proof theory
- Displaying and deciding substructural logics. I: Logics with contraposition
- Displaying modal logic
- Display logic
- Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
- Craig Interpolation in Displayable Logics
- A Unified Display Proof Theory for Bunched Logic
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Gaggles, Gentzen and Galois: how to display your favourite substructural logic
- Interpolation in fragments of classical linear logic
- Substructural logics on display
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Tools and Algorithms for the Construction and Analysis of Systems
- State of the Union: Type Inference Via Craig Interpolation