位置:成果数据库 > 期刊 > 期刊详情页
完全析取范式群判定SHOIN(D)-可满足性
  • 期刊名称:软件学报
  • 时间:0
  • 页码:1863-1877
  • 语言:中文
  • 分类:TP182[自动化与计算机技术—控制科学与工程;自动化与计算机技术—控制理论与控制工程]
  • 作者机构:[1]浙江工商大学计算机与信息工程学院,浙江杭州310018, [2]浙江大学人工智能研究所,浙江杭州310027
  • 相关基金: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 (浙江省自然科学基金)
  • 相关项目:无线网络环境中模型传输机制与图形流水线优化
中文摘要:

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

英文摘要:

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.

同期刊论文项目
同项目期刊论文