Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity
Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity
复制标题
具有交集、复合、角色反转和角色同一性的表达描述逻辑的决策过程
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
F. Massacci
中科院分区：
文献类型：
--
作者：
F. Massacci
在为现实世界应用寻求富有表现力的描述逻辑时，到目前为止，一些结构的强大组合一直困扰着实际的判定程序：角色的交集和复合。我们针对用角色的交集（∩）、复合（◦）、并集（∪）、逆（·⁻）以及角色恒等（id(·)）扩展ALC的逻辑的可满足性提出了基于表列的判定程序。我们表明：1. 通过树自动机技术给出了2 - EXPTIME上界的ALC(∩,◦,∪)的可满足性是PSPACE完全的；2. 到目前为止还是一个开放问题的ALC(∩,◦,∪, ·⁻, id(·))的可满足性在NEXPTIME内。
In the quest for expressive description logics for real-world applications, a powerful combination of constructs has so far eluded practical decision procedures: intersection and composition of roles. We propose tableau-based decision procedures for the satisfiability of logics extending ALC with the intersectionu, composition◦, uniont, converse ·− of roles and role identity id(·). We show that 1. the satisfiability of ALC(u,◦,t), for which a 2-EXPTIME upper bound was given by treeautomata techniques, is PSPACE-complete; 2. the satisfiability of ALC(u,◦,t, ·−, id(·)), an open problem so far, is in NEXPTIME.