van der Giessen, I., Jalali, R., & Kuznets, R. (2023). Extensions of K5: Proof Theory and Uniform Lyndon Interpolation. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 263–282). Springer. https://doi.org/10.1007/978-3-031-43513-3_15
E191-02 - Forschungsbereich Embedded Computing Systems
-
Published in:
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.
en
Project title:
Reasoning about Knowledge in Byzantine Distributed Systems: P 33600-N (FWF Fonds zur Förderung der wissenschaftlichen Forschung (FWF))
-
Project (external):
UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’ Netherlands Organization for Scientific Research Czech Science Foundation Grant
-
Project ID:
MR/S035540/1 639.073.807 22-06414L
-
Research Areas:
Computer Engineering and Software-Intensive Systems: 100%
CC BY 4.0
