| 摘要: |
| 针对非循环概念提出了一种对SHOIN(D)-概念可满足性进行判断的方法——CDNF(complete disjunctive normal form)算法.该算法通过把非循环定义的概念描述本身构建成分层次的析取范式群,并通过子句重用技术阻止无谓的子概念扩展,这样的析取范式群具有可满足性自明性,从而可以实现对SHOIN(D)-概念可满足性的直接判断.该算法基本上消除了判断过程中描述重复的现象,从而在空间、时间性能上都比Tableau算法有更好的表现. |
| 关键词: 描述逻辑推理 可满足性 析取范式 SHOIN(D) Tableau |
| DOI： |
| 分类号: |
| 基金项目: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 (浙江省自然科学基金) |
|
| Determining the SHOIN(D)-Satisfiability with a Complete Disjunctive Normal Form Group |
|
GU Hua-Mao,WANG Xun,LING Yun,GAO Ji
|
| 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. |
| Key words: reasoning in description logic satisfiability disjunctive normal form SHOIN(D) Tableau |
