用约束自动机解决带具体域的描述逻辑一致性问题，达到最优时间复杂度。
Robustness of Constraint Automata for Description Logics with Concrete Domains
- 用带符号约束的自动机建模，替代传统表列法
- 证明非空性判定在满足条件下属EXPTIME
- 可扩展至逆关系等特性，适合逻辑推理研究者
带有具体域的描述逻辑的一致性问题的可判定性与复杂性已通过基于表列或类型消除的方法分析。具体域在本体中对处理具体对象和预定义关系至关重要。本文提出一种基于自动机的方法，能实现最优上界EXPTIME，通过在转移中引入符号约束来增强表达能力。我们证明，若具体域满足若干简单性质，则此类自动机的非空性问题属于EXPTIME。进一步，我们给出了从本体一致性问题到该自动机非空性问题的归约，从而获得EXPTIME成员性。由于约束自动机的强表达力，结果可推广至逆角色、功能角色名及约束断言等额外成分，同时保持EXPTIME成员性，展示了该方法的鲁棒性。
原文摘要 · Abstract (English)
Decidability or complexity issues about the consistency problem for description logics with concrete domains have already been analysed with tableaux-based or type elimination methods. Concrete domains in ontologies are essential to consider concrete objects and predefined relations. In this work, we expose an automata-based approach leading to the optimal upper bound EXPTIME, that is designed by enriching the transitions with symbolic constraints. We show that the nonemptiness problem for such automata belongs to EXPTIME if the concrete domains satisfy a few simple properties. Then, we provide a reduction from the consistency problem for ontologies, yielding EXPTIME-membership. Thanks to the expressivity of constraint automata, the results are extended to additional ingredients such as inverse roles, functional role names and constraint assertions, while maintaining EXPTIME-membership, which illustrates the robustness of the approach
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。