A Step Up in Expressiveness of Decidable Fixpoint Logics
A Step Up in Expressiveness of Decidable Fixpoint Logics
复制标题
可判定定点逻辑的表达能力得到提升
DOI：
10.1145/2933575.2933592
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Benedikt M
中科院分区：
文献类型：
--
作者：
Benedikt M
守护性限制是获得可判定逻辑的主要手段之一--诸如否定这样的运算符被限制，使得自由变量包含在原子中。虽然警戒性已经在一阶逻辑的设置中卓有成效地应用，但在保留可判定性的同时添加不动点的能力非常有限。在这里，我们表明，在过去施加的主要限制之一，可以解除，得到一个更丰富的可判定的逻辑，允许不动点的参数可以不设防的不动点。使用自动机，我们证明了所得到的逻辑有一个可判定的可满足性问题，并提供了一个精细的研究复杂性的可满足性。我们表明，类似的方法适用于决定问题的逻辑公式内的不动点的消除。
Guardedness restrictions are one of the principal means to obtain decidable logics — operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.
登录
查看更多内容
论看守人员的约束力
DOI：
--
发表时间：
1999
期刊：
Journal of Symbolic Logic (JSL)
影响因子：
--
作者：
E. Grädel
通讯作者：
E. Grädel
无限树上的自动机
DOI：
10.4171/automata-1/8
发表时间：
2021
期刊：
[Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science
影响因子：
--
作者：
Christof Löding
通讯作者：
Christof Löding
受保护逻辑的有界性的复杂性
DOI：
--
发表时间：
2015
期刊：
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Michael Benedikt;B. T. Cate;Thomas Colcombet;M. V. Boom
通讯作者：
M. V. Boom
有限树上的正则成本函数
DOI：
--
发表时间：
2010
期刊：
2010 25th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Thomas Colcombet;Christof Löding
通讯作者：
Christof Löding
有界问题的可判定性结果
DOI：
10.2168/lmcs-10(3:2)2014
发表时间：
2011
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Achim Blumensath;Martin Otto;Mark Weyer
通讯作者：
Mark Weyer