An algorithm to compute maximal contractions for Horn clauses  

作　　者：LUO Jie LI Wei 

机构地区：[1]State Key Laboratory of Software Development Environment, School of Computer Science and Technology, Beihang University, Beijing 100191, China

出　　处：《Science China(Information Sciences)》2011年第2期244-257,共14页中国科学（信息科学）（英文版）

基　　金：supported by the National Basic Research Program of China (Grant No. 2005CB321901);the National High-Tech Research and Development Program of China (Grant No. 2007AA01Z146);the State Key Laboratory of Software Develop Environment Supported Project (Grant No. SKLSDE-2008ZX-01)

摘　　要：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.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.

关 键 词：maximal contraction minimal inconsistent set minimal subtraction Horn clause 

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