论文标题
喇叭的保守扩展描述具有反角色的逻辑
Conservative Extensions in Horn Description Logics with Inverse Roles
论文作者
论文摘要
我们研究了保守性扩展的可分离性和计算复杂性，以及霍恩描述逻辑（DLS）中具有反向作用的不可分割性和索引的相关概念。我们认为这两个查询保守的扩展是通过要求所有连词查询的答案保持不变的，并且具有演绎的保守性扩展，这些扩展需要构成概念包含，角色包含和功能性断言不会改变。查询保守扩展的上限尤其具有挑战性，因为通用模型之间无限制的同态象征性的特征是确定可确定性的标准方法的基础，在存在反向作用的情况下失败。我们诉诸于仔细地混合无界和有限的同构的表征，并实现结合树自动机和马赛克技术的决策程序。我们的主要结果是，在ELI和HORN-ALCHIF之间以及Horn-Alc和Horn-Alchif之间的所有DL中，查询保守的扩展都是2 impime-Complete，并且在ELI和ELHIF_ \ bot之间的所有DLS中，扣除的保守延伸均为2Exptime-Complete。不可分割性和努力的结果相同。
We investigate the decidability and computational complexity of conservative extensions and the related notions of inseparability and entailment in Horn description logics (DLs) with inverse roles. We consider both query conservative extensions, defined by requiring that the answers to all conjunctive queries are left unchanged, and deductive conservative extensions, which require that the entailed concept inclusions, role inclusions, and functionality assertions do not change. Upper bounds for query conservative extensions are particularly challenging because characterizations in terms of unbounded homomorphisms between universal models, which are the foundation of the standard approach to establishing decidability, fail in the presence of inverse roles. We resort to a characterization that carefully mixes unbounded and bounded homomorphisms and enables a decision procedure that combines tree automata and a mosaic technique. Our main results are that query conservative extensions are 2ExpTime-complete in all DLs between ELI and Horn-ALCHIF and between Horn-ALC and Horn-ALCHIF, and that deductive conservative extensions are 2ExpTime-complete in all DLs between ELI and ELHIF_\bot. The same results hold for inseparability and entailment.
