线性框架模态逻辑中 Craig 插值的非均匀视角
逻辑
2025-08-14 v2 计算机科学中的逻辑
摘要
已知扩展自线性传递框架逻辑 K4.3 的正规模态逻辑缺乏 Craig 插值性质，除了某些有界深度逻辑如 S5。我们将这一“负面”事实转化为研究问题，并通过考察以下插值存在性问题来追求 Craig 插值的非均匀方法：判定在 K4.3 之上的任意固定逻辑中，给定两个公式之间是否存在 Craig 插值。利用基于互模拟的描述框架插值存在性刻画，我们证明该问题对于所有包含 K4.3 的有限可公理化正规模态逻辑是可判定的且为 coNP-完全。因此它并不比这些逻辑中的蕴含更难，这与其他近期非均匀插值结果形成鲜明对比。我们还将我们的方法扩展到 Priorean 时序逻辑（具有过去和将来模态）在标准时间流——整数、有理数、实数和有限严格线性序——之上，这些都不具备 Craig 插值性质。
引用
@article{arxiv.2312.05929,
title = {A non-uniform view of Craig interpolation in modal logics with linear frames},
author = {Agi Kurucz and Frank Wolter and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:2312.05929},
year = {2025}
}