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

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