The Complexity of Reasoning with Boolean Modal Logics
The Complexity of Reasoning with Boolean Modal Logics
复制标题
布尔模态逻辑推理的复杂性
DOI：
10.1142/9789812776471_0018
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
U. Sattler
中科院分区：
文献类型：
--
作者：
C. Lutz;U. Sattler
布尔模态逻辑通过允许使用布尔运算符来定义复杂的关系项来扩展多模态K。在本文中，我们研究了各种这样的逻辑推理的复杂性。主要结果是：（1）在K上增加模态参数的否定使推理ExpTime完全，这是用自动机理论方法证明的;（2）在K上增加原子否定和合取甚至产生NExpTime完全逻辑，这是用多米诺骨牌问题的一个变体的简化证明的。最后的结果是相对的事实，它取决于无限数量的模态参数是可用的。如果模态参数的数目是有界的，则完全布尔模态逻辑成为ExpTime完备的。这是通过还原到富含普适模态的K来显示的。
Boolean Modal Logics extend multi-modal K by allowing the use of boolean operators to define complex relation terms. In this paper, we investigate the complexity of reasoning with various such logics. The main results are that (1) adding negation of modal parameters to K makes reasoning ExpTime-complete, which is shown by using an automata-theoretic approach, and that (2) adding atomic negation and conjunction to K even yields a NExpTime- complete logic, which is shown by a reduction of a variant of the domino problem. The last result is relativized by the fact that it depends on an infinite number of modal parameters to be available. If the number of modal parameters is bounded, full Boolean Modal Logic becomes ExpTime-complete. This is shown by a reduction to K enriched with the universal modality.