Abstract: In order to decide ABox consistency for description logic SHIN, a Tableau algorithm is presented. Given a TBox T, an ABox A and a role hierarchy H, the algorithm 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 until [A] 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]. A blocking mechanism adopted by the algorithm can avoid infinite execution of Tableau rules. The mechanism allows a new individual to be directly blocked by any individual created before it, which is not restricted to its ancestor. Through proving the termination, soundness and completeness of the algorithm, its correctness can be confirmed.

Key words: attributive language with Complement, Transitive role, role Hierarchy, Inverse role, and Number restriction（SHIN）, ABox consistency decision, Tableau algorithm, blocking mechanism, termination, soundness, completeness

摘要： 为了判定描述逻辑SHIN的ABox一致性，提出了一种Tableau算法。给定TBox T、ABox A和角色层次H，该算法通过预处理将A转换成标准的ABox [A]，按照特定的完整策略将一套Tableau规则应用于[A]，直到将它扩展成完整的ABox [A]为止。A与T和H一致，当且仅当算法能产生一个完整且无冲突的ABox [A]。算法所采用的阻塞机制可以避免Tableau规则的无限次执行，该机制允许一个新个体被在其之前创建的任意新个体直接阻塞，而不仅仅局限于其祖先。通过对算法的可终止性、合理性和完备性进行证明，算法的正确性得以确认。

关键词: 支持补集、传递角色、角色层次、反向角色和数量约束的属性语言（SHIN）, ABox一致性判定, Tableau算法, 阻塞机制, 可终止性, 合理性, 完备性