Craig interpolation in displayable logics

DOI10.1007/978-3-642-22119-4_9MaRDI QIDQ3010362zbMATH OpenOpenAlexFDO

Authors 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

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Interpolation, preservation, definability (03C40) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Machine-checked interpolation theorems for substructural logics using display calculi
• Craig interpolation for semilinear substructural logics
• Craig interpolation via hypersequents
• Craig interpolation property for operational logics of proofs
• scientific article; zbMATH DE number 2222017

Cites work

• A unified display proof theory for bunched logic
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Craig interpolation in displayable logics
• Display logic
• Displaying and deciding substructural logics. I: Logics with contraposition
• Displaying modal logic
• Failure of interpolation in relevant logics
• Gaggles, Gentzen and Galois: how to display your favourite substructural logic
• Handbook of proof theory
• Harmonious logic: Craig's interpolation theorem and its descendants
• scientific article; zbMATH DE number 1927419 (Why is no real title available?)
• scientific article; zbMATH DE number 970628 (Why is no real title available?)
• Interpolation in fragments of classical linear logic
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• State of the Union: Type Inference Via Craig Interpolation
• Substructural logics on display
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(10)

• Multicomponent proof-theoretic method for proving interpolation properties
• Craig interpolation in the presence of unreliable connectives
• Hypersequent and display calculi -- a unified perspective
• Preservation of Craig interpolation by the product of matrix logics
• Machine-checked interpolation theorems for substructural logics using display calculi
• Proving Craig and Lyndon interpolation using labelled sequent calculi
• Craig interpolation in displayable logics
• Interpolation via translations
• scientific article; zbMATH DE number 910750 (Why is no real title available?)
• Internal and external calculi: ordering the jungle without being lost in translations

This page was built for publication: Craig interpolation in displayable logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3010362)