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

摘要

To decide ABox consistency for SHIF, this paper presented a Tableau algorithm. The algorithm first converted ABox into a standard form by pre-disposal, and then applied a set of Tableau rules to ABox according to specific completion strategies until it extended to a complete ABox. ABox was consistent with regard to TBox if and only if the algorithm could yield a clash-free and complete ABox. It adopted a blocking mechanism by the algorithm could avoid infinite execution of Tableau rules. To raise the efficiency of the algorithm, the mechanism allowed a new individual to be directly blocked by any individual created before it, which was not restricted to its ancestor. Through proving the termination, soundness and completeness of the algorithm, confirmed its correctness.%为了判定SHIF的ABox一致性,提出了一种Tableau算法.该算法先通过预处理将ABox转换成标准形式,然后按照特定的完整策略将一套Tableau规则应用于ABox,直到将它扩展成完整的ABox为止.ABox与TBox一致,当且仅当算法能产生一个无冲突的完整的ABox.算法所采用的阻塞机制可以避免Tableau规则的无限次执行.为了提高算法的效率,该机制允许一个新个体被在其之前创建的任意新个体直接阻塞,而不仅仅局限于其祖先.通过对算法的可终止性、合理性和完备性进行证明,算法的正确性得以确认.