|
|
计算机应用 2009
Research on Tableau algorithm for Horn-Extended DL
|
Abstract:
描述逻辑和逻辑程序是两种非常重要的知识表达形式,分别具有不同的表达能力.为了保证结合描述逻辑和逻辑程序的可判定性,Motik给出了一种DL-safe规则.在Motik工作的基础上,提出了对描述逻辑进行Horn子句拓展的Horn-Extended DL,并给出了Horn-Extended DL的Tableau算法,最后通过一个算例验证了算法的正确性和效率.
