完全析取范式检测ALCN-概念的可满足性  

Checking the Satisfiability of ALCN-concepts with a Complete DNF

作　　者：古华茂[1,2] 高济[2] 王勋[1] 

机构地区：[1]浙江工商大学信息学院,浙江杭州310018 [2]浙江大学人工智能研究所,浙江杭州310027

出　　处：《四川大学学报（工程科学版）》2009年第6期165-170,共6页Journal of Sichuan University (Engineering Science Edition)

基　　金：国家自然科学基金(60775029);国家高技术研究发展计划(863)(2007AA01Z187);国家重点基础研究发展规划(973)(2003cb31700);浙江省科技计划(2007C33072);浙江省自然科学基金(Y1090734)资助项目

摘　　要：基于"逐步展开"模式的Tableau算法在各类非循环定义的描述逻辑概念的可满足性判断中会产生大量的重复性的中间概念描述,因而浪费大量的空间。为此,提出了一个全新的对非循环定义的ALCN-概念可满足性进行判断的完全析取范式(CDNF)算法。CDNF算法直接在输入概念描述上,以角色为纽带构建不同层次的析取范式,从而将输入概念描述重组成一种层次结构的可满足性直接可知的完全析取范式,从而实现了真正意义上的"计算"可满足性。CDNF算法采用"一步到位"的展开方式并且直接在输入概念描述上进行处理,因而可最大程度地消除概念描述的重复。因此,CDNF算法比Tableau算法能节省线性甚至指数倍于输入概念描述长度的空间代价。The Tableaux based on 'unfolding gradually' may produce a lot of repetitive intermediate concept descriptions in deciding the satisfiabilities of acyclic concepts in a variety of description logics,which wastes large space.To tackle this problem,a novel Complete Disjunctive Normal Form(CDNF) algorithm was presented to check the satisfiabilities of acyclic ALCN-concepts.CDNF algorithm built disjunctive normal forms connected by roles in different levels directly on input concept description,and reorganized t...

关 键 词：可满足性推理 析取范式 ALCN 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]