一句话：为 K、T、K4、S4 的 Horn/Krom/core 等亚命题片段建立表达力层级，并证明无 diamond 的 Horn 片段可满足性为多项式时间。
本文研究模态逻辑 K、T、K4 与 S4 的若干亚命题片段，包括经典 Horn 片段、Krom 片段、二者交得到的 core 片段，以及通过限制子句中 box 与 diamond 使用而得到的子片段。作者首先关注这些语言的相对表达力：引入一种适合的表达力度量，并构建出一个覆盖所考虑逻辑全部片段的复杂层级。随后，鉴于特别是不含 diamond 的 Horn 片段表达力较低，文章转向其可满足性问题的计算复杂度，证明该问题在一般情况下为多项式时间。结果刻画了模态逻辑在限制命题连接词后表达力与判定复杂度之间的权衡。
In this paper, we consider the well-known modal logics $\mathbf{K}$, $\mathbf{T}$, $\mathbf{K4}$, and $\mathbf{S4}$, and we study some of their sub-propositional fragments, namely the classical Horn fragment, the Krom fragment, the so-called core fragment, defined as the intersection of the Horn and the Krom fragments, plus their sub-fragments obtained by limiting the use of boxes and diamonds in clauses. We focus, first, on the relative expressive power of such languages: we introduce a suitable measure of expressive power, and we obtain a complex hierarchy that encompasses all fragments of the considered logics. Then, after observing the low expressive power, in particular, of the Horn fragments without diamonds, we study the computational complexity of their satisfiability problem, proving that, in general, it becomes polynomial.
@article{paperbot399,
title = {On Sub-Propositional Fragments of Modal Logic},
author = {Davide Bresolin and Emilio Muñoz-Velasco and Guido Sciavicco},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 2},
year = {2018},
doi = {10.23638/lmcs-14(2:16)2018}
}