具有并、复合和差运算的有限二元关系代数中可满足性的不可判定性
计算机科学中的逻辑
2014-06-03 v1 数据库
摘要
我们考虑使用并、复合和集合差运算符由二元关系名称构建的表达式。我们证明了测试给定此类表达式 是否有限可满足(即是否存在可代入关系名称的有限二元关系,使得 的计算结果为非空)是不可判定的。该结果在仅提及单个关系名称且差运算符嵌套次数至多为一次的表达式限制下依然成立。
引用
@article{arxiv.1406.0349,
title = {Undecidability of satisfiability in the algebra of finite binary relations with union, composition, and difference},
author = {Tony Tan and Jan Van den Bussche and Xiaowang Zhang},
journal= {arXiv preprint arXiv:1406.0349},
year = {2014}
}