On two-variable guarded fragment logic with expressive local Presburger constraints
arxiv(2022)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要