Extensions of \textsf{K5}: proof theory and uniform Lyndon interpolation

DOI10.1007/978-3-031-43513-3_15MaRDI QIDQ6541157zbMATH OpenFDO

Authors Iris van der Giessen, Raheleh Jalali, Roman Kuznets

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43513-3_15

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• An algebraic theory of normal forms
• Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
• Craig interpolation via hypersequents
• Deep sequent systems for modal logic
• Grafting hypersequents onto nested sequents
• scientific article; zbMATH DE number 4108725 (Why is no real title available?)
• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 2024614 (Why is no real title available?)
• scientific article; zbMATH DE number 219032 (Why is no real title available?)
• scientific article; zbMATH DE number 922620 (Why is no real title available?)
• Interpolation for intermediate logics via hyper- and linear nested sequents
• Interpolation for intermediate logics via injective nested sequents
• Modal interpolation via nested sequents
• Modal logic
• Multicomponent proof-theoretic method for proving interpolation properties
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• On some calculi of modal logic
• Proving Craig and Lyndon interpolation using labelled sequent calculi
• Simplified Kripke-style semantics for some normal modal logics
• The decidability of normal K5 logics
• The extensions of the modal logic K5
• Undefinability of propositional quantifiers in the modal system S4
• Uniform interpolation and propositional quantifiers in modal logics
• Uniform interpolation and the existence of sequent calculi
• Uniform interpolation via nested sequents
• Uniform Lyndon interpolation for basic non-normal modal logics
• Uniform Lyndon interpolation for intuitionistic monotone modal logic
• Uniform Lyndon interpolation property in propositional modal logics

Cited in

(2)

• Uniform interpolation via nested sequents and hypersequents
• Mechanised uniform interpolation for modal logics K, GL, and iSL

This page was built for publication: Extensions of \textsf{K5}: proof theory and uniform Lyndon interpolation

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