完全析取范式群判定SHOIN(D)-可满足性

摘要：

针对非循环概念提出了一种对SHOIN(D)-概念可满足性进行判断的方法--CDNF(complete disjunctive normal form)算法.该算法通过把非循环定义的概念描述本身构建成分层次的析取范式群,并通过子句重用技术阻止无谓的子概念扩展,这样的析取范式群具有可满足性自明性,从而可以实现对SHOIN(D)-概念可满足性的直接判断.该算法基本上消除了判断过程中描述重复的现象,从而在空间、时间性能上都比Tableau算法有更好的表现.

关键词：描述逻辑推理、可满足性、析取范式、SHOIN(D)、Tableau

所属期刊栏目：21

分类号：TP182(自动化基础理论)

资助基金：the National Natural Science Foundation of China under Grant Nos.60775029, 60873218;the National High-Tech Research and Development Plan of China under Grant No.2007AA01Z187 国家高技术研究发展计划863;the Zhejiang Provincal Natural Science Foundation of China under Grant No.Y1090734

在线出版日期：2010-09-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共15页

页码：1863-1877