带等号的一致一维片段的复杂性与表达能力
逻辑
2014-09-03 v1 计算机科学中的逻辑
摘要
一致一维片段 UF1^= 是一种形式体系，其通过对一阶逻辑中的量词应用加以限制而获得，即仅允许使用存在量词（或全称量词）块，使得被量化公式中至多保留一个自由变量。该片段在布尔运算下封闭，但对包含两个或更多变量的原子公式的组合施加了额外的限制（称为一致性条件）。该片段可视为双变量逻辑的规范推广，旨在处理任意元数的关系。该片段是近期提出的，已有研究证明不含等号的 UF1^= 片段的可满足性问题是可判定的。本文确立了 UF1^= 的可满足性和有限可满足性问题均为 NEXPTIME-完全。我们还表明，带有计数量词的 UF1^= 扩展版本的相应问题是不可判定的。除了可判定性问题外，我们还比较了 UF1^= 与带有计数量词的双变量逻辑 FOC^2 的表达能力。我们证明，虽然这两种逻辑在一般情况下不可比较，但当词汇表的元数限制为二时，UF1^= 严格包含于 FOC^2 中。
引用
@article{arxiv.1409.0731,
title = {Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality},
author = {Emanuel Kieroński and Antti Kuusisto},
journal= {arXiv preprint arXiv:1409.0731},
year = {2014}
}
备注
preprint