线性框架与自然数上单调混合逻辑的复杂性
计算复杂性
2012-06-13 v2
摘要
带约束变量的混合逻辑是一种表达力强的规约语言。其可满足性问题在一般情况下是不可判定的。如果框架限制为 N 或一般线性序，则可满足性已知是可判定的，但具有非初等复杂性。在本文中，我们考虑 N 和一般线性序上的单调混合逻辑（即布尔联结词仅为合取与析取）。我们证明，在线性序上可满足性问题仍保持非初等复杂性，但在 N 上其复杂性降至 PSPACE-完全。我们将由不同模态和混合算子组合产生的严格片段分类为 NP-完全和易处理的（即 NC1 或 LOGSPACE 完全的）。有趣的是，NP-完全性仅取决于片段，而与框架无关。对于 NP 以上的情况，线性序上的可满足性比 N 上更难，而在 NP 以下则至多一样难。此外，我们考察了所讨论片段的模型论性质。
引用
@article{arxiv.1204.1196,
title = {The Complexity of Monotone Hybrid Logics over Linear Frames and the Natural Numbers},
author = {Stefan Göller and Arne Meier and Martin Mundhenk and Thomas Schneider and Michael Thomas and Felix Weiss},
journal= {arXiv preprint arXiv:1204.1196},
year = {2012}
}
备注
19 pages + 15 pages appendix, 3 figures