描述逻辑的具象域约束自动机鲁棒性
计算机科学中的逻辑
2026-01-28 v1 人工智能
摘要
关于描述逻辑的具象域一致性问题的可判定性或复杂度问题，已通过表算法或类型消除法进行分析。具象域在本体中至关重要，用于考虑具体对象和预定义关系。在本工作中，我们揭示了一种基于自动机的方法，达到最优上界 EXPTIME，方法通过为转换添加符号约束来实现。我们证明，若具象域满足若干简单属性，则此类自动机的非空问题属于 EXPTIME。随后，我们提供了从本体一致性问题的归约，得到 EXPTIME 成员。由于约束自动机的表达力，这些结果扩展到诸如逆角色、函数角色名称和约束断言等附加要素，同时保持 EXPTIME 成员，这说明了该方法的鲁棒性。
引用
@article{arxiv.2601.19644,
title = {Robustness of Constraint Automata for Description Logics with Concrete Domains},
author = {Stéphane Demri and Tianwen Gu},
journal= {arXiv preprint arXiv:2601.19644},
year = {2026}
}
备注
Extended version of a paper accepted at CSL'26, Paris