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

• 作者: 凌云 古华茂 王勋 高济
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 描述逻辑推理 可满足性 析取范式 SHOIN(D) Tableau
• 年，卷（期）: 2010,（8）
• 页码范围: 1863-1877
• 分类号: TP182
• 字数: 17932字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2010.03597

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	高济	浙江大学人工智能研究所	113	1578	22.0	34.0
2	王勋	浙江工商大学计算机与信息工程学院	28	216	7.0	14.0
3	凌云	浙江工商大学计算机与信息工程学院	25	314	9.0	17.0
4	古华茂	浙江工商大学计算机与信息工程学院	10	82	4.0	9.0