On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations
On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations
复制标题
具有等价关系的二变量一阶逻辑的有限可满足性
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Lidia Tendera
中科院分区：
文献类型：
--
作者：
Emanuel Kieronski;Lidia Tendera
我们证明了每一个具有两个等价关系的有限可满足的二变量一阶公式都有一个关于其长度的大小最多为三指数的模型。因此，具有两个等价关系的结构类上的二变量逻辑的有限可满足性问题在不确定的三指数时间内是可确定的。我们也证明了用一个只需要传递的关系来代替被考虑的结构类中的一个等价关系会导致不可判定。这强化了先前的结果，即双变量逻辑在具有两个传递关系的结构类上是不可判定的。
We show that every finitely satisfiable two-variable first-order formula with two equivalence relations has a model of size at most triply exponential with respect to its length. Thus the finite satisfiability problem for two-variable logic over the class of structures with two equivalence relations is decidable in nondeterministic triply exponential time. We also show that replacing one of the equivalence relations in the considered class of structures by a relation which is only required to be transitive leads to undecidability. This sharpens the earlier result that two-variable logic is undecidable over the class of structures with two transitive relations.