Craig Interpolation in Displayable Logics

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

Mathematics Subject Classification ID

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