 Journal of Computer and Communications, 2013, 1, 20-25 http://dx.doi.org/10.4236/jcc.2013.15004 Published Online October 2013 (http://www.scirp.org/journal/jcc) Copyright © 2013 SciRes. JCC One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property* Wei Li1, Yuefei Sui2 1State Key Laboratory of Software Development Environment, Beijing University of Aeronautics and Astronautics, Beijing, China; 2Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China. Email: liwei@nlsde.buaa.edu.cn, yfsui@ict.a c.cn Received July 2013 ABSTRACT The AGM axiom system is for the belief revision (revision by a single belief), and the DP axiom system is for the iterated revision (revision b y a finite sequence of beliefs). Li  gave an R-calculus for R-configurations |,∆Γ where ∆ is a set of atomic formulas or the negations of atomic formulas, and Γ is a finite set of formulas. In propositional logic programs, one R-calculus N will be given in this paper, such that N is sound a nd complete w ith r espect to op erator ( ,)st∆, where ( ,)st∆ is a pseudo-theory minimal change of t by ∆. Keywords: Belief Revision; R-Calculus; Soundness and Completeness of a Calculus; Pseudo-Subtheory 1. Introduction The AGM axiom system is for the belief revision (revision by a single belief) [2-5], and the DP axiom system is for the iterated revision (revision by a finite sequence of beliefs) [6,7]. These postulates list some basic requirements a revision operator ΓΦ (a result of theory Γ revised by Φ) should satisfy. The R-calculus () gave a Gentzen-type deduction system to deduce a consistent one ′Γ ∪∆ from an in- consistent theory ,Γ∪∆ where ′Γ ∪∆ should be a maximal consistent subtheory of Γ∪∆ which includes ∆ as a subset, where |∆Γ is an R-configuration, Γ is a consistent set of formulas, and ∆ is a consistent sets of atomic formulas or the negation of atomic for- mulas. It was proved that if ||′∆Γ⇒∆Γ is deducible and |′∆Γ is an R-termination, i.e., ther e is no R-rule to reduce |′∆Γ to another R-configuration |,′′∆Γ then ′∆∪Γ is a contraction of Γ by .∆ The R-calculus is set-inclusion, that is, ,Γ∆ are ta- ken as belief b ases, not as belief s ets [8-11]. In the follow- ing we shall take ,∆Γ as belief bases, not belief sets. We shall define an operator (, ),st∆ where ∆ is a set of theories and t is a theory in propositional logic programs, such that • ,( ,)st∆∆ is consistent; • ( ,)st∆ is a pseudo-subt he o r y of ;t • ( ,)st∆ is maximal such that ,( ,)st∆∆ is consistent, and for any pseudo-subtheory η of ,t if ( ,)st∆ is a pseudo-subtheory of η and η is not a pseudo- subtheory of η then either ,( ,)stη∆∆ and ,( ,),stη∆∆ or ,η∆ is inconsistent. Then, we give one R-calculus N such that N is sound and complete with respect to operator (, ),st∆ where  N is sound with respect to operator (, ),st∆ if |,ts∆ ⇒∆ being provable implies =(, ),ss t∆ and  N is complete with respect to operator (, ),st∆ if |,( ,)t st∆ ⇒∆∆ is prova ble. Let  be the pseudo-subtheory relation, ()Pt be the set of all the pseudo-subtheories of ,t and ∆≡ be an equivalence relation on ()Pt such that for any 121 2,( ),Ptηηη η∆∈≡ iff 12, ,.ηη∆∆ Given a pseudo-subtheory ,tη let []η be the equivalence class of r with respect to .∆≡ About the minimal change, we prove that [(, )]st∆ is -maximal in ( )/Pt∆≡ such that ,( ,)st∆∆ is con- sistent, that is, ♦ ,( ,)st∆∆ is consistent; and ♦ for any η such that [(,)][] [],st tη∆ either [][(, )]stη∆ or ,η∆ is inconsistent. [(, )]st∆ being -maximal implies that ( ,)st∆ is a minimal change of t by ∆ in the syntactical sense, not in the set-theoretic sense, i.e., ( ,)st∆ is a minimal change of t by ∆ in the theoretic form such that ( ,)st∆ *This work was supported by the Open Fund of the State Key Labora- tory of Software Develop ment Environment under Grant No. SKLSDE- 2010KF-06, Beijing University of Aeronautics and Astronautics, and by the National Basic R esearch Progr am of China (97 3 Program) under Grant No. 2005CB321901. One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property Copyright © 2013 SciRes. JCC 21 is consistent with .∆ The paper is organized as follows: the next section gives the basic elements of the R-calculus and the de- finition of subtheories and pseudo-subtheories; the third section defines the R-calculus N; the fourth section prov- es that N is sound and complete with respect to the operator (, );st∆ the fifth section discusses the logical properties of t and (, ),st∆ and the last section con- cludes the whole paper. 2. The R-Calculus The R-calculus () is defined on a first-order logical language. Let L′ be a logical language of the first-order logic; ,ϕψ formulas and ,Γ∆ sets of formulas (the- ories), where ∆ is a set of atomic formulas or the ne- gations of atomic formulas. Given two theories Γ and ,∆ let |∆Γ be an R- configura tion. The R-calculus consists of the following axiom and inference rules: cut 12 2212 12( ),|,,|,,|, |() |, ,|,|, |() |, ||,||,|() |, ||,||,|() |,||[ /],|() |, |Ttxxϕϕ ϕϕ ψϕψψχχϕϕϕψϕψϕψϕψϕψϕϕ¬∧∨→∀∆¬Γ ⇒∆ΓΓΓ∆Γ⇒∆ Γ∆ ΓΓ⇒∆ΓΓ∆Γ⇒∆ Γ∆∧Γ⇒∆ Γ∆Γ⇒∆ Γ∆Γ⇒∆ Γ∆∨Γ⇒∆ Γ∆¬Γ⇒∆ Γ ∆Γ⇒∆Γ∆→Γ⇒∆ Γ∆Γ⇒∆ Γ∆ ∀Γ⇒∆ ΓARRRRR where in cut ,TϕψR means that ϕ occurs in the proof tree T of ψ from 1Γ and ;ϕ and in ,Rt∀ is a term, and is free in ϕ for x. Definition 2.1. ||′′∆ Γ⇒∆Γ is an R-theorem, denoted by | |,R′′∆ Γ⇒∆Γ if there is a sequence {( ,,,):}iii iin′′∆Γ∆ Γ≤ such that (i) ||= ||,nnnn′′′′∆ Γ⇒∆Γ∆Γ⇒∆Γ (ii) for each 1,in≤≤ either ||ii ii′′∆Γ⇒∆Γ is an axiom, or ||ii ii′′∆Γ⇒∆Γ is deduced by some R-rule of form 11 11||||ii iiii ii−− −−′′∆Γ⇒∆Γ′′∆Γ⇒∆Γ. Definition 2.2. ||′∆Γ⇒∆Γ is valid, denoted by | |,′∆Γ⇒∆Γ if for any contraction Θ of ′Γ by ,∆Θ is a contraction of Γ by .∆ Theorem 2.3(The soundness and completeness the- orem of the R-calculus). For any theories ,′ΓΓ and ,∆ ||′∆Γ⇒∆Γ if and only if | |.′∆Γ⇒∆Γ Theorem 2.4. The R-rules preserve the strong validity. Let L be the logical language of the propositional logic. A literal l is an atomic formula or the negation of an atomic formula; a clause c is the disjunction of finitely many literals, and a theory t is the conjunction of finitely many clauses. Definition 2.5. Given a theory ,t a theory s is a sub-theory of ,t denote d by ,st if either =,ts or (i) if 1=tt¬ then 1;st (ii) if 21=ttt ∧ then either 1st or 2;st and (iii) if 12=tcc∨ then either 1sc or 2.sc Let = ()().tpqp q′′∨∧ ∨ Then, ,;p qpqt′′∨∨ and ,, ().ppqpp pqt′ ′′′∧ ∧∧∨ Definition 2.6. Given a theory 1[ ,...,],ntss where 1s is an occurrence of 1s in ,t a theory 1= [,...,]= [/,...,/],ns ttssλλλ λ where the occurrence is is replaced by the empty theory ,λ is called a pseu- do-subtheory of ,t denoted by .st Let = ()().tpqp q′′∨∧ ∨ Then, ,,,, ().pqpqp pqpppqt′′′ ′′′∨∨∧∧∧∨ Proposit ion 2.7. For any theories 12 1,,tts and 2,s (i) 11st implies 1 12s tt∨ and 1 12;s tt∧ (ii) 11st and 22st imply 11121 2,stsstt¬¬∨ ∨ and 1 212.ss tt∧∧ Proposition 2.8. For any theories t and ,s if st then .st Proof. By the induction on the structure of .t Proposition 2.9.  and  are partial orderings on the set of all the theories. Given a theory ,t let ()Pt be the set of all the pseu- do-subtheories of .t Each ()s Pt∈ is determined by a set 1()= {[],...,[]},nsp pτ where each []ip is an occurrence of ip in ,t such that 1= ([]/,...,[]/).ns tppλλ Given any 12,(),s sPt∈ define 121 2121 2= max{:,};= min{:,}.s sssssss ssssss   Proposit ion 2.10. For any pseudo-subtheories 121 2,(),s sPtss∈ and 12ss exist. Let ()=((), ,,, )Pt Pttλ be the lattice with the greatest element t and the least element .λ Proposit ion 2.11. For any pseudo-subtheories 121 2,(),s sPtss∈ if and only if 12( )().ssττ⊇ More- over, 121 2121 2()=()();()=()().sss ssss sτ τττ ττ∪∩ One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property Copyright © 2013 SciRes. JCC 22 3. The R-Calculus N The deduct ion system N: 12111 2121 122121 2() ()|, |,|,()| ,|| ,|,() |,aallNNll ltsNt tstc dcdNcc ddλ∧∨∆¬ ∆¬∆ ⇒∆∆ ⇒∆∆ ⇒∆∆∧ ⇒∆∆⇒∆ ∆⇒∆∆∨⇒∆∨ where ,t∆ denotes a theory { };tλ∆∪ is the empty string, and if s is consistent then ,ssssssλλλλλ∨≡∨ ≡∧≡∧ ≡∆ ≡∆ and if s is inconsistent then ssssλ λλλ λλ∨≡∨ ≡∧≡∧ ≡ Definition 3.1. |,ts∆ ⇒∆ is N-provable if there is a statement sequence }1:,|{ nistiiii≤≤∆⇒∆ such that |,= |,,nn nnts ts∆ ⇒∆∆⇒∆ and for each ,in≤ |,ii iits∆ ⇒∆ is either by an aN- rule or by an N∧-,or N∨-rule. An exam pl e is the follo w i ng deduction for 1 1212|, :lllll¬ ∨∨¬ 11 11 2121 12121212 11212 21212 121211212121212||,| ,,,| ,,| ,,| ,| ,,|,.ll ll llll llllllll lllll lllll lllllllll llllllλ¬ ⇒¬¬ ⇒¬¬∨⇒ ¬∨≡¬¬ ⇒¬¬ ¬⇒¬¬∨ ¬⇒¬¬∨∨¬⇒ ¬∨¬⇒¬ Notice that 11 1|ll l¬ ⇒¬ and 1 1212() ().l llll≡∨∧∨¬ Theorem 3.2. For any theory set ∆ and theory ,t there is a theory s such that |,ts∆ ⇒∆ is N-prova- ble. Proof. We prove the theorem by the induction on the structure of .t If =tl is a literal then either l∆¬ or .l∆¬ If l∆¬ then |,lλ∆ ⇒∆ and =;sλ if l∆¬ then |,ll∆ ⇒∆ and =;sl If 12=ttt∧ then by the induction assumption, there are theories s1, s2 such that 11|,ts∆ ⇒∆ and 12 12, |,,.s tss∆ ⇒∆ Therefore, 1 212| ,,t tss∆∧ ⇒∆ and 12=.sss∧ If 12=tcc∨ then by the induction assumption, there are theories 12,ss such that 11|,cs∆ ⇒∆ and 22| ,.cs∆ ⇒∆ Therefore, 12 12|,cc ss∆∨ ⇒∆∨ and 12=.sss∨ Proposition 3.3. If |,ts∆ ⇒∆ is N-provable then .st Proof. We prove the proposition by the induction on the length of the proof of | ,.ts∆ ⇒∆ If the last rule used is 1()aN then =,tl and = =;sltl If the last rule used is 2()aN then =,tl and = =;s tlλ If the last rule used is ()N∧ then 11|,ts∆⇒∆ and 12 12, |,,.s tss∆ ⇒∆ By the induction assumption, 11st and 22.st Hence, 1 212=;sstt t∧∧ If the last rule used is ()N∧ then 11|,cs∆ ⇒∆ and 22| ,.cs∆ ⇒∆ By the induction assumption, 11st and 22.st Hence, 12 12=.sscc t∨∨ Proposition 3.4. If |,ts∆ ⇒∆ is N-provable then {}s∆∪ is consistent. Proof. We prove the proposition by the induction on the length of the proof of | ,.ts∆ ⇒∆ If the last rule used is 1()aN then ,l∆¬ and | ,.ll∆ ⇒∆ Then, {}l∆∪ is consistent; If the last rule used is 2()aN then ,l∆¬ and | ,.lλ∆ ⇒∆ Then, {}λ∆∪ is consistent; If the last rule used is ()N∧ then 11|,ts∆⇒∆ and 12 12, |,,.s tss∆ ⇒∆ By the induction assumption, 1{}s∆∪ and 12{, }ss∆∪ is consistent, and so is 12{}={};ss s∆∧ ∆∪∪ If the last rule used is ()N∨ then 11|,cs∆ ⇒∆ and 22| ,.cs∆ ⇒∆ By the induction assumption, 1{}s∆∪ and 2{}s∆∪ is consistent, and so is 12{}={}.ss s∆∨ ∆∪∪ 4. The Completeness of the R-Calculus N For any theory t, def ine ( ,)st∆ as follows: 1 12121 212if= andif= and(, )=(,) ({(,)},)if =(,)(,)if =tl lltl lst st sstttt tst sttttλ∆¬∆¬∆∆ ∧∆∆∧∆ ∨∆∨∪ About the inconsistence, we have the following facts: • if l∆¬ then {}l∆∪ is inconsistent; • 12{}tt∆∧∪ is inconsistent if and only if either 1{}t∆∪ is inconsistent or 12{, }tt∆∪ is in- con- sistent; • 12{}cc∆∨∪ is inconsistent if and only if both 1{}c∆∪ and 2{}c∆∪ are inconsistent. One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property Copyright © 2013 SciRes. JCC 23 Proposition 4.1. For any consistent th eory set ∆ and a theory ,{ (,)}t st∆∆∪ is consistent. Proof. We prove the proposition by the induction on the structure of .t If =tl and l is consistent with ∆ then (, )=sll∆ is consistent with ;∆ if =tl and l is inconsistent with ∆ then (, )=slλ∆ is consistent with ;∆ If 12=ttt∧ then by the induction assumption, 1{ (,)}st∆∆∪ and 1 12{ (,),({(,)},)}sts stt∆∆ ∆∆∪∪ are consistent, so 12{ (,)}stt∆ ∆∧∪ is consistent; If 12=tcc∨ then by the induction assumption, 1{ (,)}sc∆∆∪ and 2{ (,)}sc∆∆∪ are consistent, so 121 2{(,)}={(, )(,)}sccsc sc∆∆∨ ∆∆∨∆∪∪ is consis- tent. About the consistence, we have the following facts: • if l∆¬ then {}l∆∪ is consistent; • 12{}tt∆∧∪ is consistent if and only if 1{}t∆∪ is consistent and 12{, }tt∆∪ is consistent; • 12{}cc∆∨∪ is consistent if and only if either 1{}c∆∪ or 2{}c∆∪ is consistent. Theorem 4.2. If {}t∆∪ is consistent then ,( ,)ts t∆∆ and ,( ,).stt∆∆ Proof. We prove the theorem by the induction on the structure of .t If =tl and l is consistent with ∆ then (, )=,sll∆ and the theorem holds for ;l If 12=ttt∧ then 1{}t∆∪ and 12{, }tt∆∪ is con- sistent, and by the induction assumption, 1111121 212 2, (,),(,) ;,,({ },), ({ },),t stst tstss ts stt∆∆∆∆∆∆∆∆∪∪ where 11=( ,).sst∆ Henc e, 1 21121121 2,( ,)({ },), (,)({},).t tstsststsstt t∆ ∧∆∧∆∆ ∆∧∆∧∪∪ If 12=tcc∨ then either 1{}c∆∪ or 12{, }cc∆∪ is consistent, and by the induction assumption, either 1111,(, ),(, );c scsc c∆∆∆∆ or 2222,(, ),(, ).c scscc∆∆∆∆ Hence, we have 121 212 12,(, )(,),(, )(,).ccsc scsc sccc∆ ∨∆∨∆∆ ∆∨∆∨ Theorem 4.3. |,ts∆ ⇒∆ is N-provable if and only if =(, ).ss t∆ Proof. ()⇒ Assume that |,ts∆ ⇒∆ is N-provable. We assume that for any <,in the claim holds. If =tl and the last rule is 1()aN then l∆¬ and | ,.ll∆ ⇒∆ It is clear that ==(, );sls l∆ If =tl and the last rule is 2()aN then l∆¬ and | ,.lλ∆ ⇒∆ It is clear that ==(, );sslλ∆ If 12=ttt∧ and the last rule is ()N∧ then 11|,ts∆⇒∆ and 121212|, |,,.ttstss∆∧ ⇒∆⇒∆ By the induction assumption, 11( ,)=st s∆ and 12 2({},) =.sst s∆∪ Then, 1211212==(,) ({},)=(,);sssstsststt∧∆∧∆∆ ∧∪ If 12=tcc∨ and the last rule is ()N∨ then 11|,cs∆ ⇒∆ and 22| ,.cs∆ ⇒∆ By the induction assumption, 1 122=( ,),=(,),sscssc∆∆ and 12 1212==(,)(,)=(,).ssssc scscc∨∆∨∆∆ ∨ ()⇐ Let =(, ).ss t∆ We prove that |,ts∆ ⇒∆ is N-provable by the induction on the structure of .t If =tl and l∆¬ then (, )=,slλ∆ and | ,,lλ∆ ⇒∆ i.e., | ,;ls∆ ⇒∆ If =tl and l∆¬ then (, )=,sll∆ and | ,,ll∆ ⇒∆ i.e., | ,;ls∆ ⇒∆ If 12=ttt∧ then 1211 2(,)=(,) ({(,)},).sttst sstt∆ ∧∆∧∆∆∪ By the induc- tion assumption, 11| ,(,)t st∆⇒∆ ∆ and 12112,|,,({ (,)},).s tssstt∆⇒∆∆ ∆∪ Therefore, 1211 2|,,({ (,)},);t tssstt∆∧ ⇒∆∆∆∪ If 12=tcc∨ then 1211 2(,)=(, )({(, )},).sccsc sscc∆ ∨∆∨∆∆∪ By the in- duction assumption, 11|,(, )c sc∆⇒∆ ∆ and 22|, (,).csc∆⇒∆∆ Therefore, 121 2|,(, )(,).ccscsc∆∨⇒∆∆∨ ∆ 5. The Logical Properties of t and (),st∆ It is clear that we have the following Proposit ion 5.1. For any theory set ∆ and theory ,t ( ,)(,).tstξ∆∆ Theorem 5.2. For any theory set ∆ and theory ,t ,( ,)(,);,( ,)( ,).t stst tξξ∆∆ ∆∆∆ ∆ Proof. By the definitions of (,),(,)stξξ∆∆ and the induction on the structure of .t Proposition 5.3. (i) If ,( ,)stt∆∆  then ,t∆ is in- consistent; (ii) If ,( ,)stt∆∆ then ,t∆ is consistent. Define = {():{}isconsistent};= {():{}isinconsistent}.ttCsPtsIsPts∆∆∈∆∈∆∪∪ Then, = ()ttC IPt∆∆∪ and =.ttCI∆∆∅∩ Define an equivalence relation ∆≡ on ()tP such that for any 12,(),s sPt∈ 121 2iff,, .sss s∆≡ ∆∆ One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property Copyright © 2013 SciRes. JCC 24 Given a pseudo-subtheory ( ),s Pt∈ let []r be the equivalence class of .s Then, we ha ve that [ (, )],[(, )].tsttCξ∆∆ ∆⊆ Proposit ion 5.4. [(, )]=[(, )].st tξ∆∆ Define a relation  on )(tP such that for any 1s and 2 12( ),sPt ss∈ iff 12112 211 22 122111 21 1222111 122212211 221221112112221111222122=if ===&= or=&=if =and==&= or=&=if=and =llsland slcccc ccccsc csccssss ssssss ssss∨∨∧∧ Proposition 5.5.  is an equivalence relation on ( ),Pt and for any 12,(),s sPt∈ if 12ss then 12.ss Theorem 5.6. If |,ts∆ ⇒∆ is provable then for any η with ,| ,st sηη∆ ⇒∆ is prova ble. Proof. We prove the theorem by the induction on the structure of .t If =tl and l∆¬ then =,sλ and for any η with ,=,stη ηλ and |,ηλ∆ ⇒∆ is prova ble; If =tl and l∆¬ then =,sl and for any η with , =,s tlηη and |,sη∆ ⇒∆ is prova ble; If 12=ttt∧ and the theorem holds for both 1t and 2t then 12=,sss∧ and for any η with ,stη there are 1η and 2η such that 1 11stη and 2 22.stη By the induction assumption, 111 212|,,, |,,,ssssηη∆⇒∆ ∆⇒∆ and by ()N∧, 12121 2|,, , ;sss sηη∆∧⇒∆≡∆ ∧ If 12=tcc∨ and the theorem holds for both 1c and 2c then 12=,sss∨ and for any η with ,stη there are 1η and 2η such that 111scη and 222.scη By the induction assumption, 1 122| ,;|,,ssηη∆⇒∆ ∆⇒∆ and by ()N∨, 1 212| ,.ssηη∆∨⇒∆ ∨ Theorem 5.7. For any η with ,stη if ,η∆ is consistent then , ,,sη∆∆ and hence, [] = [];sη and if ,η∆ is inconsistent then , ,,tη∆∆ and hence, [] = [].tη Proof. If ,η∆ is consistent then by Theorem 6.6, | ,,sη∆ ⇒∆ and we prove by the induction on the structure of t that , ,.ts∆∆ If =tl and l∆¬ then =,sl and , ,;ts∆∆ If 12=ttt∧ and the claim holds for both 1t and 2t then 12 11= ,,,sss ts∧∆∆ and 22, ,.ts∆∆ There- fore, 1212, ,.tt ss∆∧∆∧ If 21=cct ∨ and the theorem holds for both 1c and 2c then 12=,ddd∨ and there are three cases: Case 1. 1,c∆ and 2,c∆ are consistent. By the in- duction a s s umption , we ha ve that 1 122,, ,,,,c dcd∆ ∆∆∆  and hence, 1212, ,;cc dd∆∨ ∆∨ Case 2. 1,c∆ is consistent and 2,c∆ is inconsistent. By the induction assumption, we have that 11, ,,cd∆∆ and 2|.c∆ ⇒∆ Then, 1 12112,,;d ddccc∆≡∆ ∨∨ and 121211112,( )(),,ccc cccddd∆∨≡∆∧∨ ∆∧≡ ∆∧≡∆ ∨ where 2=.dλ Case 3. Similar to Case 2. Corollary 5.8. For any η with ,stη either ][=][ sη or [] = [].tη Therefore, []s is -maximal such that s,∆ is consistent. 6. Conclusions and Further Works We defined an R-calculus N in propositional logic pro- grams such that N is sound and complete with respect to the operator (, ).st∆ The following axiom is one of the AGM postulates: Extensionality :ifthen=pqKp Kq It is satisfied, because we have the following Proposit ion 7.1. If 1 2111;| ,ttt sts⇒ and 2 22|,t sts⇒ then 12.ss It is not true in N that (*) if 1 211;| ,sststs′⇒ and 22|,tsts′⇒ then 12.ss′′ A further work is to give an R-calculus having the property ()∗. A simplified form of ()∗ is (**) if 121 1;| ,sststs′⇒ and 22|,tsts′⇒ then 12,ss′′ which is not true in N either. Another further work is to give an R-calculus having the property ()∗∗ and havin g not the property ()∗. REFERENCES  W. Li, “R-Calculus: An Inference System for Belief Re-vision,” The Computer Journal, Vol. 50, 2007, pp. 378- 390. http://dx.doi.org/10.1093/comjnl/bxl069  C. E. Alchourrón, P. Gärdenfors and D. Makinson, “On the Logic of Theory Change: Partial Meet Contraction and Revision Functions,” Journal of Symbolic Logic, Vol. 50, 1985, pp. 510-530. http://dx.doi.org/10.2307/2274239  A. Bochman, “A Foundational Theory of Belief and Be-lief Change,” Artificial Intelligence, Vol. 108, 1999, pp. 309-352. http://dx.doi.org/10.1016/S0004-3702(98)00112-X  M. Dalal, “Investigations into a Theory of Knowledge One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property Copyright © 2013 SciRes. JCC 25 Base Revision: Preliminary Report,” Proceedings of AAAI-88, St. Paul, 1988, pp. 475-479.  P. Gärdenfors and H. Rott, “Belief Revision,” In: D. M. Gabbay, C. J. Hogger and J. A. Robinson, Eds., Hand-book of Logic in Artificial Intelligence and Logic Pro-gramming, Vol. 4, Epistemic and Temporal Reasoning, Oxford Science Pub., 1995, pp. 35-132.  A. Darwiche and J. Pearl, “On the Logic of Iterated Belief Revision,” Artificial Intelligence, Vol. 89, 1997, pp. 1-29. http://dx.doi.org/10.1016/S0004-3702(96)00038-0  E. Fermé and S. O. Hansson, “AGM 25 Years, Twenty- Five Years of Research in Belief Change,” Journal of Philosophical Logic, Vol. 40, 2011, pp. 295-331. http://dx.doi.org/10.1007/s10992-011-9171-9  N. Friedman and J. Y. Halpern, “Belief Revision: A Criti- que,” In: L. C. Aiello, J. Doyle and S. C. Shapiro, Eds., Journal of of Logic, Language and Information, Princi- ples of Knowledge Representation and Reasoning, Pro-ceedings of the 5th Conference, 1996, pp. 421-431.  S. O. Hansson, “Theory Contraction and Base Contrac-tion Unified,” Journal of Symbolic Logic, Vol. 58, 1993, pp. 602-626. http://dx.doi.org/10.2307/2275221  A. Herzig and O. Rifi, “Propositional Belief Base Update and Minimal Change,” Artificial Intelligence, Vol. 115, 1999, pp. 107-138. http://dx.doi.org/10.1016/S0004-3702(99)00072-7  K. Satoh, “Nonmonotonic Reasoning by Minimal Belief Revision,” Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, 1988, pp. 455-462.