FO^2 with one transitive relation is decidable
FO^2 with one transitive relation is decidable
复制标题
具有一个传递关系的 FO^2 是可判定的
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Lidia Tendera
中科院分区：
文献类型：
--
作者：
W. Szwast;Lidia Tendera
我们证明了在传递结构上的二元一阶逻辑FO^2的可满足性问题是可判定的，当只需要一个关系是传递的。这个结果是最优的，因为已知具有两个传递关系或具有一个传递关系和一个等价关系的结构上的FO^2是不可判定的，所以实际上，我们的结果完成了传递结构上的FO^2-逻辑在可判定性方面的分类。
我们表明，可满足性问题是在2-NExpTime。
有限可满足性问题的可判定性仍然是开放的。
We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability.
We show that the satisfiability problem is in 2-NExpTime.
Decidability of the finite satisfiability problem remains open.