一种子句重构的增强Tableau算法  

An Enhanced Tableau Algorithm Based on Clause Reorganization

作　　者：古华茂[1,2] 高济[1] 王勋[2] 吴海燕[2] 

机构地区：[1]浙江大学人工智能研究所,杭州310027 [2]浙江工商大学计算机与信息工程学院,杭州310018

出　　处：《模式识别与人工智能》2009年第4期532-540,共9页Pattern Recognition and Artificial Intelligence

基　　金：国家自然科学基金项目(No.60775029);国家863计划项目(No.2007AA01Z187);浙江省科技计划项目(No.2007C33072)资助

摘　　要：利用非循环定义的概念可展开的特性,提出一个基于子句重构的增强Tableau算法.采用最简洁的概念合取子句代替原来的子概念集对完整树/图上的结点进行标记,并设计一组推理规则以构建这样的完整树/图,从而消除传统Tableau算法中的∩-规则、∪-规则所带来的概念描述重复.因而在非循环定义概念可满足性判定问题上,空间性能有明显提高.此外,虽然文中只提供针对SI语言的规则和证明,可是这种处理思路同样适用于其它描述逻辑语言,因而具有一定的推广价值.Taking advantage of the expandability of acyclic concept definitions, an enhanced Tableau algorithm based on clause reorganization is presented. It substitutes the succinctest conjunctive clause of concepts for sub-concepts set in labeling nodes of complete tree/graph. To build a new complete tree/graph, a set of reasoning rules is designed, which avoids tremendous description redundancy caused by ∩-rules and ∪ -rules of the traditional Tableau. Thus, the spatial performance of judging the satisfiabilities of acyclic concept definitions is improved greatly. In this papers only reasoning rules and proofs designated for SI language are provided. However, the idea of enhancement mode is suitable for various DL well, which makes it much valuable languages

关 键 词：增强Tableau 描述逻辑推理 可满足性 合取子句 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]