horn-extendeddl的tableau算法研究

？描述逻辑和逻辑程序是两种非常重要的知识表达形式，分别具有不同的表达能力。为了保证结合描述逻辑和逻辑程序的可判定性，motik给出了一种dl-safe规则。在motik工作的基础上，提出了对描述逻辑进行horn子句拓展的horn-extendeddl，并给出了horn-extendeddl的tableau算法，最后通过一个算例验证了算法的正确性和效率。