Proving Craig and Lyndon interpolation using labelled sequent calculi
From MaRDI portal
Publication:2835880
DOI10.1007/978-3-319-48758-8_21zbMATH Open1485.03091arXiv1601.05656OpenAlexW2963340765MaRDI QIDQ2835880FDOQ2835880
Authors: Roman Kuznets 
Publication date: 30 November 2016
Published in: Logics in Artificial Intelligence (Search for Journal in Brave)
Abstract: We have recently presented a general method of proving the fundamental logical properties of Craig and Lyndon Interpolation (IPs) by induction on derivations in a wide class of internal sequent calculi, including sequents, hypersequents, and nested sequents. Here we adapt the method to a more general external formalism of labelled sequents and provide sufficient criteria on the Kripke-frame characterization of a logic that guarantee the IPs. In particular, we show that classes of frames definable by quantifier-free Horn formulas correspond to logics with the IPs. These criteria capture the modal cube and the infinite family of transitive Geach logics.
Full work available at URL: https://arxiv.org/abs/1601.05656
Recommendations
Modal logic (including the logic of norms) (03B45) Interpolation, preservation, definability (03C40)
Cites Work
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Proof Analysis
- Modal logic for philosophers
- Geometrisation of first-order logic
- Partition-based logical reasoning for first-order and propositional theories
- Multi-dimensional modal logic
- Modal interpolation via nested sequents
- Uniform Interpolation by Resolution in Modal Logic
- Beth definability in expressive description logics
- Absence of the interpolation property in the consistent normal modal extensions of the Dummett logic
- Craig interpolation in displayable logics
- A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi
- The logic of exact covers: completeness and uniform interpolation
- Interpolation method for multicomponent sequent calculi
- Labelled tree sequents, tree hypersequents and nested (deep) sequents
- Title not available (Why is that?)
Cited In (12)
- Through an inference rule, darkly
- Lyndon Interpolation for Modal $$\mu $$-Calculus
- Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
- Multicomponent proof-theoretic method for proving interpolation properties
- Craig’s trick and a non-sequential system for the Lambek calculus and its fragments
- Interpolation method for multicomponent sequent calculi
- Interpolation for intermediate logics via hyper- and linear nested sequents
- Modal interpolation via nested sequents
- Craig interpolation via hypersequents
- Uniform Lyndon interpolation property in propositional modal logics
- Horn filter pairs and Craig interpolation in propositional logic
- Extensions of \textsf{K5}: proof theory and uniform Lyndon interpolation
This page was built for publication: Proving Craig and Lyndon interpolation using labelled sequent calculi
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2835880)
