Two-Variable First-Order Logic with Equivalence Closure
Two-Variable First-Order Logic with Equivalence Closure
复制标题
具有等价闭包的二变量一阶逻辑
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Lidia Tendera
中科院分区：
文献类型：
--
作者：
Emanuel Kieronski;Jakub Michaliszyn;Ian Pratt;Lidia Tendera
我们考虑一阶逻辑的二变量片段扩展的可满足性和有限可满足性问题，其中等价闭包运算符可以应用于固定数量的二元谓词。我们证明了将等价闭包应用于两个二元谓词的双变量一阶逻辑的可满足性问题在 2NEXPTIME 中，并且通过表明存在两个等价关系的情况下双变量一阶逻辑的可满足性问题是 2NEXPTIME-hard 来获得匹配下界。所讨论的逻辑缺乏有限模型属性；然而，我们表明相同的复杂性界限适用于相应的有限可满足性问题。我们进一步表明，将等价闭包应用于单个二元谓词的一阶逻辑的双变量片段的可满足性（=有限可满足性）问题是 NEXPTIME 完全的。
We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2NEXPTIME, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2NEXPTIME-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite satisfiability problems. We further show that the satisfiability (=finite satisfiability) problem for the two-variable fragment of first-order logic with equivalence closure applied to a single binary predicate is NEXPTIME-complete.