Multicomponent proof-theoretic method for proving interpolation properties

DOI10.1016/j.apal.2018.08.007OpenAlexW2889405014WikidataQ129333489 ScholiaQ129333489MaRDI QIDQ1799040

Roman Kuznets

Publication date: 18 October 2018

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2018.08.007

zbMATH Keywords

modal logicCraig interpolationstructural proof theoryhypersequentlabelled sequentLyndon interpolation

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03) Interpolation, preservation, definability (03C40)

Related Items (3)

Uniform interpolation via nested sequents ⋮ Interpolation in extensions of first-order logic ⋮ Through an Inference Rule, Darkly

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9--13, 2013
• Interpolation systems for ground proofs in automated deduction: a survey
• Hypersequent rules with restricted contexts for propositional modal logics
• Prefixed tableaus and nested sequents
• Modal interpolation via nested sequents
• An interpolation theorem in the predicate calculus
• Modal tableau calculi and interpolation
• Proof analysis in modal logic
• Deep sequent systems for modal logic
• Gentzen calculi for modal propositional logic
• The many faces of interpolation
• Proof methods for modal and intuitionistic logics
• Absence of the interpolation property in the consistent normal modal extensions of the Dummett logic
• Der Interpolationssatz der intuitionistischen Prädikatenlogik
• Amalgamation and interpolation in normal modal logics
• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• Cut-free sequent calculi for some tense logics
• Indexed systems of sequents and cut-elimination
• Multi-dimensional modal logic
• Skolem's discovery of Gödel-Dummett logic
• Circular proofs for the Gödel-Löb provability logic
• On some calculi of modal logic
• GEOMETRISATION OF FIRST-ORDER LOGIC
• Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
• Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5
• Failure of Interpolation in Constant Domain Intuitionistic Logic
• Craig Interpolation in Displayable Logics
• A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi
• Proof Analysis
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Uniform Interpolation by Resolution in Modal Logic
• A constructive analysis of RM
• Natural 3-valued logics—characterization and proof theory
• CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT
• Grafting hypersequents onto nested sequents
• Hypersequent Calculi for Godel Logics -- a Survey
• From Frame Properties to Hypersequent Rules in Modal Logics
• The Logic of Exact Covers: Completeness and Uniform Interpolation
• Interpolation Method for Multicomponent Sequent Calculi
• Computer Aided Verification
• Analytic tableau systems and interpolation for the modal logics KB, KDB, K5, KD5

This page was built for publication: Multicomponent proof-theoretic method for proving interpolation properties