一个无可行模型性质的可靠一阶模态逻辑捆绑片段
计算机科学中的逻辑
2025-06-03 v1
摘要
一阶模态逻辑（\FOML）的可满足性问题即使对于仅含一元谓词、两个变量等简单片段也是不可判定的。近期，一种识别 \FOML 可判定片段的新方法被提出，称为“捆绑片段”，其中量词与模态词被限制为同时出现。由于存在多种将量词捆绑在一起的方式，其中一些会导致可判定或不可判定的片段。在 (Liu et al., 2023) 中，作者证明了一个“三分法”，表明每个捆绑片段属于以下三类之一：(1) 满足“有限模型性质”（因而可判定），(2) 不可判定，以及 (3) 不满足“有限模型性质”（其可判定性尚悬而未决）。在本文中，我们通过证明属于最后一类的唯一组合确实是可判定的，从而在“递增域模型”上将该三分法坍缩为二分法。
引用
@article{arxiv.2506.01421,
title = {A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property},
author = {Varad Joshi and Anantha Padmanabha},
journal= {arXiv preprint arXiv:2506.01421},
year = {2025}
}