The sound and complete R-calculus for revising propositional theories  

作　　者：LI Wei SUI YueFei SUN MeiYing 

机构地区：[1]State Key Laboratory of Software Development Environment, Beihang University [2]Key Laboratory of Intelligent Information Processing, Institute of Computing Technology,Chinese Academy of Sciences [3]University of Chinese Academy of Sciences

出　　处：《Science China(Information Sciences)》2015年第9期1-12,共12页中国科学（信息科学）（英文版）

基　　金：supported by Open Fund of the State Key Laboratory of Software Development Environment,Beihang University(Grant No.SKLSDE-2010KF-06);National Basic Research Program of China(973Program)(Grant No.2005CB321901)

摘　　要：The AGM postulates are for the belief revision （revision by a single belief）, and the DP postulates for the iterated revision （revision by a finite sequence of beliefs）. Li gave an R-calculus for R-configurations △｜Г, where A is a set of atomic formulas or the negations of atomic formulas, and F is a finite set of formulas. In this paper, two deduction systems for the revision of a theory by another theory are given such that the systems are sound and complete, that is, if △｜Г → Г′ is provable then Г′ △ is consistent and Г′ - △ is a maximal subset of F such that （Г′ - △） tO A is consistent; and for any finite theories A and F, there is a finite theory Fl such that Г′ - A is a maximal subset of F such that （Г′ - △） ∪ △ is consistent, and △｜Г → Г′ is provable. Moreover, if △｜Г → Г′ is provable then Г′ satisfies the AGM and the DP postulates.The AGM postulates are for the belief revision （revision by a single belief）, and the DP postulates for the iterated revision （revision by a finite sequence of beliefs）. Li gave an R-calculus for R-configurations △｜Г, where A is a set of atomic formulas or the negations of atomic formulas, and F is a finite set of formulas. In this paper, two deduction systems for the revision of a theory by another theory are given such that the systems are sound and complete, that is, if △｜Г → Г′ is provable then Г′ △ is consistent and Г′ - △ is a maximal subset of F such that （Г′ - △） tO A is consistent; and for any finite theories A and F, there is a finite theory Fl such that Г′ - A is a maximal subset of F such that （Г′ - △） ∪ △ is consistent, and △｜Г → Г′ is provable. Moreover, if △｜Г → Г′ is provable then Г′ satisfies the AGM and the DP postulates.

关 键 词：belief revision R-calculus minimal change the AGM postulates the DP postulates 

分 类 号：O141.1[理学—数学]