描述逻辑ALC基于RBox的推理  

RBox Reasoning in Description Logic ALC

作　　者：王雪瑞[1] 李拴保[2] 

机构地区：[1]河南工程学院计算机科学与技术学院,河南新郑451191 [2]河南财政税务高等专科学校信息工程系,河南郑州451464

出　　处：《湘潭大学自然科学学报》2014年第2期104-108,共5页Natural Science Journal of Xiangtan University

摘　　要：针对RBox表达能力受限于简单角色的问题,研究了在角色包含公式中允许出现一类由合取和析取构造子连接的复杂角色,并且TBox和ABox均为空集的情况下ALC概念的可满足性问题,设计了可满足性检测表算法,分析了算法的终止性,证明了可靠性和完备性,最后讨论了复杂度.理论分析表明,此时ALC概念的可满足性问题是可判定的,并且复杂度为ExpTime.Aiming at the restriction of RBox expressiveness which is caused by atom roles,satisfiability of ALC concept is discussed on condition that RBox permits a kind of special complex role connected by intersection/union constructors to exist in role inclusion axioms and both TBox and ABox are empty.A tableau algorithm for checking satisfiability is presented and its termination is analyzed.Then,proof of soundness and completeness of the algorithm is given and its complexity is also investigated.The theoretical analysis shows that ALC satisfiability is still decidable in this situation and complexity is in ExpTime class.

关 键 词：描述逻辑 角色包含公式 可满足性 表算法 复杂度 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]