K5的扩展：证明论与一致Lyndon插值
计算机科学中的逻辑
2024-03-01 v1 逻辑
摘要
我们引入了一种称为分层相继式演算的Gentzen风格框架，用于模态逻辑K5及其扩展KD5、K45、KD45、KB5和S5，旨在研究一致Lyndon插值性质（ULIP），该性质同时蕴含一致插值性质和Lyndon插值性质。我们为所有上述逻辑获得了复杂度最优的决策过程，并给出了K5的ULIP的构造性证明，据我们所知，这是首个此类语法证明。为证明插值子的正确性，我们使用了模型论方法，特别是模文字的双模拟。
引用
@article{arxiv.2307.11727,
title = {Extensions of K5: Proof Theory and Uniform Lyndon Interpolation},
author = {Iris van der Giessen and Raheleh Jalali and Roman Kuznets},
journal= {arXiv preprint arXiv:2307.11727},
year = {2024}
}
备注
20-page conference paper + 5-page appendix with examples and proofs