The two-variable fragment with counting and equivalence
The two-variable fragment with counting and equivalence
复制标题
具有计数和等价性的二变量片段
DOI：
10.1002/malq.201400102
复制
发表时间：
2015
影响因子：
0.3
通讯作者：
Pratt-Hartmann I
中科院分区：
文献类型：
--
作者：
Pratt-Hartmann I
我们考虑一阶计数逻辑的两变量片段，服从一个单独的二元谓词被解释为等价的规定。我们证明了这个逻辑的可满足性和有限可满足性问题都是NExpTime-完全的。进一步证明了具有计数和两个等价的二元一阶逻辑的相应问题都是不可判定的.
We consider the two‐variable fragment of first‐order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are bothNExpTime‐complete. We further show that the corresponding problems for two‐variable first‐order logic with counting andtwoequivalences are both undecidable.