带传递性的单目否定片段的有限可满足性
计算机科学中的逻辑
2019-07-01 v3
摘要
我们证明了具有任意数量传递关系的单目否定片段的有限可满足性问题是可判定的且为2-ExpTime完全的。我们的结果实际上在一个更一般的设定下成立，其中可要求某些二元符号解释为任意传递关系，某些为偏序，某些为等价关系。我们还考虑了我们主要逻辑的各种扩展的有限可满足性，特别是捕获了来自描述逻辑的指称（nominals）与角色层次（role hierarchies）概念。由于单目否定片段可表达合取查询的并，我们的结果对有限查询应答问题具有有趣的含义，无论是在经典场景还是在描述逻辑设定中。
引用
@article{arxiv.1809.03245,
title = {Finite Satisfiability of Unary Negation Fragment with Transitivity},
author = {Daniel Danielski and Emanuel Kieronski},
journal= {arXiv preprint arXiv:1809.03245},
year = {2019}
}
备注
Accepted for MFCS 2019