###
DOI:
Journal of Software:2010.21(8):1863-1877

完全析取范式群判定SHOIN(D)-可满足性
古华茂,王勋,凌云,高济
(浙江工商大学 计算机与信息工程学院,浙江 杭州 310018;浙江大学 人工智能研究所,浙江 杭州 310027)
Determining the SHOIN(D)-Satisfiability with a Complete Disjunctive Normal Form Group
GU Hua-Mao,WANG Xun,LING Yun,GAO Ji
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3672   Download 3262
Received:July 31, 2008    Revised:February 16, 2009
> 中文摘要: 针对非循环概念提出了一种对SHOIN(D)-概念可满足性进行判断的方法——CDNF(complete disjunctive normal form)算法.该算法通过把非循环定义的概念描述本身构建成分层次的析取范式群,并通过子句重用技术阻止无谓的子概念扩展,这样的析取范式群具有可满足性自明性,从而可以实现对SHOIN(D)-概念可满足性的直接判断.该算法基本上消除了判断过程中描述重复的现象,从而在空间、时间性能上都比Tableau算法有更好的表现.
Abstract:This paper presents an approach to check the satisfiability of acyclic SHOIN(D)-concepts—CDNF (complete disjunctive normal form) algorithm. This calculus can make a direct judgment on the satisfiability of acyclic SHOIN(D)-concept by restructuring it into a hierarchical disjunctive normal form group on concept descriptions which is satisfiability self-telling, and reusing description clauses to block unnecessary extensions. CDNF algorithm eliminates description overlaps to the largest extent for it works on concept description directly. Therefore, CDNF algorithm has much better performance than Tableau as it saves a lot of spatial and temporal costs.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by 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 (浙江省自然科学基金) Supported by 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 (浙江省自然科学基金)
Foundation items:
Reference text:

古华茂,王 勋,凌 云,高 济.完全析取范式群判定SHOIN(D)-可满足性.软件学报,2010,21(8):1863-1877

GU Hua-Mao,WANG Xun,LING Yun,GAO Ji.Determining the SHOIN(D)-Satisfiability with a Complete Disjunctive Normal Form Group.Journal of Software,2010,21(8):1863-1877