论文部分内容阅读
为判定描述逻辑SHIQ的ABox一致性，提出一种Tableau算法。给定TBox几ABoxA和角色层次H，通过预处理将A转换成标准的ABox A’，按照特定的完整策略将一套Tableau规则应用于A，从而不断地对A’进行扩展，直到将其扩展成完整的ABoxA”为止。A、T和H一致，当且仅当算法能产生一个完整且无冲突的ABox A”。该算法采用的阻塞机制能防止Tableau规则被无限次执行，避免多余的规则应用。通过证明Tableau规则的执行次数为有限次，确认算法的可终止性。通过证明由A”能构造一个同时满足A