多智能体模态逻辑统一插值性质的证明论方法
计算机科学中的逻辑
2025-10-30 v1
摘要
统一插值性质(UIP)是Craig插值性质的一种加强。它最初由Pitts(1992)基于纯证明论方法建立。多模态、和逻辑中的UIP已通过语义方法建立，然而，证明论方法仍然缺乏。Bílková (2007)发展了Pitts (1992)的方法来证明经典模态逻辑和中的UIP。本文进一步扩展了Bílková (2007)的系统，以建立多智能体模态逻辑、和中的UIP。提出了一个纯语法算法来确定一个统一插值公式。还表明，在这些系统中，对命题变元的量化可以通过UIP来建模。此外，还提出了一个不使用二阶量词直接建立UIP的论证。
引用
@article{arxiv.2510.25394,
title = {A proof-theoretic approach to uniform interpolation property of multi-agent modal logic},
author = {Youan Su},
journal= {arXiv preprint arXiv:2510.25394},
year = {2025}
}