论文标题
在两变量的保护片段逻辑上，具有富有表现力的本地前爆发约束
On two-variable guarded fragment logic with expressive local Presburger constraints
论文作者
论文摘要
我们考虑使用本地前堡定量器扩展两变量的保护片段逻辑。这些是可以表达属性的量词，例如“传入的蓝色边缘的数量以及两倍的外向红色边缘的数量最多是传入的绿色边缘的数量”，并捕获了用计数的各种描述逻辑，但没有恒定的符号。我们表明，此逻辑的满足性问题是Expolede。虽然下边界已经适用于标准的两变量守卫片段逻辑，但上限是由一种新颖而又简单的基于图形的算法建立的。
We consider the extension of the two-variable guarded fragment logic with local Presburger quantifiers. These are quantifiers that can express properties such as "the number of incoming blue edges plus twice the number of outgoing red edges is at most three times the number of incoming green edges" and captures various description logics with counting, but without constant symbols. We show that the satisfiability problem for this logic is EXP-complete. While the lower bound already holds for the standard two-variable guarded fragment logic, the upper bound is established by a novel, yet simple deterministic graph-based algorithm.
