%0 Journal Article
%T horn-extendeddl的tableau算法研究
%A 肖岚
%A 郑力
%A 肖建
%A 黄毅
%J 计算机应用
%D 2009
%X ？描述逻辑和逻辑程序是两种非常重要的知识表达形式，分别具有不同的表达能力。为了保证结合描述逻辑和逻辑程序的可判定性，motik给出了一种dl-safe规则。在motik工作的基础上，提出了对描述逻辑进行horn子句拓展的horn-extendeddl，并给出了horn-extendeddl的tableau算法，最后通过一个算例验证了算法的正确性和效率。
%K 描述逻辑
%K 逻辑程序
%K 模型理论语义
%K horn子句
%K tableau算法
%U http://www.joca.cn/CN/abstract/abstract11188.shtml