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