文件名称：一种描述逻辑SHIF的ABox一致性判定算法 (2013年)
文件大小：682KB
文件格式：PDF
更新时间：2024-06-07 08:43:52
工程技术 论文
为了判定SHIF的ABox一致性, 提出了一种Tableau算法。该算法先通过预处理将ABox转换成标准形式, 然后按照特定的完整策略将一套Tableau规则应用于ABox, 直到将它扩展成完整的ABox为止。ABox与TBox一致, 当且仅当算法能产生一个无冲突的完整的ABox。算法所采用的阻塞机制可以避免Tableau规则的无限次执行。为了提高算法的效率, 该机制允许一个新个体被在其之前创建的任意新个体直接阻塞, 而不仅仅局限于其祖先。通过对算法的可终止性、合理性和完备性进行证明, 算法的正确性得以确