Interpolation method for multicomponent sequent calculi

DOI10.1007/978-3-319-27683-0_15MaRDI QIDQ5283429zbMATH OpenOpenAlexFDO

Authors Roman Kuznets

Publication date 21 July 2017

Published in Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-27683-0_15

zbMATH Keywords

sequent calculiCraig interpolationhypersequent calculiLyndon interpolationnested sequent calculi

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Multicomponent proof-theoretic method for proving interpolation properties
• Interpolation for intermediate logics via hyper- and linear nested sequents
• Modal interpolation via nested sequents
• Craig interpolation via hypersequents
• Proving Craig and Lyndon interpolation using labelled sequent calculi

Cites work

• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 5263148 (Why is no real title available?)
• scientific article; zbMATH DE number 3199779 (Why is no real title available?)
• Absence of the interpolation property in the consistent normal modal extensions of the Dummett logic
• Cut-free hypersequent calculus for S4.3.
• From Frame Properties to Hypersequent Rules in Modal Logics
• Modal interpolation via nested sequents
• Nested sequents for intuitionistic logics
• Proof methods for modal and intuitionistic logics
• Proving Craig and Lyndon interpolation using labelled sequent calculi
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

Cited in

(9)

• Through an inference rule, darkly
• Uniform interpolation via nested sequents
• Multicomponent proof-theoretic method for proving interpolation properties
• Modal interpolation via nested sequents
• Interpolation for intermediate logics via hyper- and linear nested sequents
• Craig interpolation via hypersequents
• Interpolation via translations
• Interpolation in practical formal development
• Proving Craig and Lyndon interpolation using labelled sequent calculi

This page was built for publication: Interpolation method for multicomponent sequent calculi

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