描述逻辑SHIQ的ABox一致性判定算法

ABox Consistency Decision Algorithm for Description Logic SHIQ

为判定描述逻辑SHIQ的ABox一致性,提出一种Tableau算法。给定TBox T、ABox A和角色层次H,通过预处理将A转换成标准的ABox A’,按照特定的完整策略将一套Tableau规则应用于A’,从而不断地对A’进行扩展,直到将其扩展成完整的ABox A’’为止。A、T和H一致,当且仅当算法能产生一个完整且无冲突的ABox A’’。该算法采用的阻塞机制能防止Tableau规则被无限次执行,避免多余的规则应用。通过证明Tableau规则的执行次数为有限次,确认算法的可终止性。通过证明由A’’能构造一个同时满足A、T和H的解释,确认算法的合理性。通过证明Tableau规则的执行不会破坏A’与H的一致关系,确认算法的完备性。

In order to decide ABox consistency for Description Logic（DL） SH1Q, a Tableau algorithm is presented. Given a TBox T, an ABox A and a role hierarchy H, the algorithm first converts A into a standard ABox A＇ by pre-disposal, and then applies a set of Tableau rules to A＇ according to specific completion strategies, thus A＇ is extended continually, until it is extended to a complete ABox A＂. A is consistent with T and H, if and only if the algorithm can yield a complete and clash-free ABox A＂. The blocking mechanism adopted by the algorithm can prevent Tableau rules＇ unlimited execution, and avoid redundant rule application. By proving Tableau rules＇ execution times is limited, the algorithm＇s termination is ensured. By proving Tableau rules＇ excecution is unlikely to destroy the consistency between A＇ and H, the algorithm＇s soundness is ensured. By proving an explanation which satisfies A, T and H can be constructed in terms of A＂, the algorithm＇s completeness is ensured.