一个在Horn子句中求解极大缩减的算法  

An algorithm to compute maximal contractions for Horn clauses

作　　者：罗杰[1] 李未[1] 

机构地区：[1]北京航空航天大学计算机学院软件开发环境国家重点实验室,北京100191

出　　处：《中国科学：信息科学》2011年第2期129-143,共15页Scientia Sinica(Informationis)

基　　金：国家重点基础研究发展计划(批准号:2005CB321901);国家高技术研究发展计划(批准号:2007AA01Z146);软件开发环境国家重点实验室自主课题(批准号:SKLSDE-2008ZX-01)资助项目

摘　　要：在信念修正理论中,一个核心问题是求解一个公式集合关于事实集合的所有极大协调子集,即极大缩减.本文尝试从算法的角度来解决这一问题,研究在Horn子句中求解所有极大缩减的算法.首先,本文指出并证明了公式集合和事实集合并集的极小不协调子集与公式集合关于事实集合的极大缩减之间的转化关系.其次,给出并证明了Horn子句集合极小不协调的一个必要条件.然后,基于上述两个结论,本文提出了一个在Horn子句中枚举公式集合和事实集合并集的极小不协调子集的交互式算法和一个通过这些极小不协调子集计算所有极大缩减的算法.最后,综合这两个算法,提出了一个在Horn子句中求解所有极大缩减的交互式算法.In the theory of belief revision,the computation of all maximal subsets（maximal contractions） of a formula set with respect to a set of facts is one of the key problems.In this paper,we try to solve this problem by studying the algorithm to compute all maximal contractions for Horn clauses.First,we point out and prove the conversion relationship between minimal inconsistent subsets of union of the formula set and the set of facts and maximal contractions of the formula set with respect to the set of facts.Second,we prove a necessary condition of a set of Horn clauses to be minimal inconsistent.Then,based on these two conclusions,we propose an interactive algorithm to enumerate all minimal inconsistent subsets of a given set of Horn clauses and a second algorithm to compute maximal contractions from these minimal inconsistent subsets.Finally,we proposed an interactive algorithm to compute maximal contractions for Horn clauses by composing the above two algorithms.

关 键 词：极大缩减 极小不协调集合 极小减集 HORN子句 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]