典范模型与模态团队逻辑的复杂性
计算机科学中的逻辑
2023-06-22 v5
摘要
我们研究了模态团队逻辑 MTL，它是模态逻辑 ML 在团队语义下的扩展，并在布尔否定下封闭。其片段，如模态依赖逻辑、独立逻辑和包含逻辑，已得到充分理解。然而，由于无限制的布尔否定，完整 MTL 的可满足性问题一直难以进行复杂性理论分类。在我们的方法中，我们将典范模型的概念引入团队语义设置。通过构建此类模型，我们将 MTL 的可满足性问题归约为简单的模型检测。随后，我们证明了该方法在意义上是最优的，即 MTL 公式可以有效地强制典范性。此外，为了在复杂性方面捕捉这些结果，我们引入了一个非初等复杂性类 TOWER(poly)，并证明它包含作为完全问题的 MTL 可满足性和有效性。我们还证明了具有有界模态深度的 MTL 片段对于初等层次（具有多项式数量的交替）的各个层级是完全的。相应的硬度结果适用于模态算子和分裂析取的严格或宽松语义，也适用于自反和传递框架类。
引用
@article{arxiv.1709.05253,
title = {Canonical Models and the Complexity of Modal Team Logic},
author = {Martin Lück},
journal= {arXiv preprint arXiv:1709.05253},
year = {2023}
}