Journal of Computer and Communications, 2013, 1, 2025 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 RCalculus with PseudoSubtheory 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 [1] gave an Rcalculus for Rconfigurations 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 Rcalculus N will be given in this paper, such that N is sound a nd complete w ith r espect to op erator , where is a pseudotheory minimal change of by . Keywords: Belief Revision; RCalculus; Soundness and Completeness of a Calculus; PseudoSubtheory 1. Introduction The AGM axiom system is for the belief revision (revision by a single belief) [25], 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 calculus ([1]) gave a Gentzentype 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 Rconfiguration, 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 Rtermination, i.e., ther e is no Rrule to reduce to another Rconfiguration then is a contraction of by The calculus is setinclusion, that is, are ta ken as belief b ases, not as belief s ets [811]. In the follow ing we shall take as belief bases, not belief sets. We shall define an operator where is a set of theories and is a theory in propositional logic programs, such that • is consistent; • is a pseudosubt he o r y of • is maximal such that is consistent, and for any pseudosubtheory of if is a pseudosubtheory of and is not a pseudo subtheory of then either and or is inconsistent. Then, we give one calculus N such that N is sound and complete with respect to operator where N is sound with respect to operator if being provable implies and N is complete with respect to operator if is prova ble. Let be the pseudosubtheory relation, be the set of all the pseudosubtheories of and be an equivalence relation on such that for any iff Given a pseudosubtheory let be the equivalence class of with respect to About the minimal change, we prove that is maximal in such that is con sistent, that is, ♦ is consistent; and ♦ for any such that either or is inconsistent. being maximal implies that is a minimal change of t by in the syntactical sense, not in the settheoretic sense, i.e., is a minimal change of t by in the theoretic form such that *This work was supported by the Open Fund of the State Key Labora tory of Software Develop ment Environment under Grant No. SKLSDE 2010KF06, Beijing University of Aeronautics and Astronautics, by the National Basic R esearch Progr am of China (97 3 Grant No. 2005CB321901.
One Sound and Complete RCalculus with PseudoSubtheory Minimal Change Property Copyright © 2013 SciRes. JCC is consistent with The paper is organized as follows: the next section gives the basic elements of the Rcalculus and the de finition of subtheories and pseudosubtheories; the third section defines the Rcalculus N; the fourth section prov es that N is sound and complete with respect to the operator the fifth section discusses the logical properties of t and and the last section con cludes the whole paper. 2. The RCalculus The Rcalculus ([1]) is defined on a firstorder logical language. Let ′ be a logical language of the firstorder 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 Rcalculus consists of the following axiom and inference rules: cut 12 22 12 12 ( ),,, ,,,  () , ,, ,  () ,  ,, () ,  ,, () , [ /], () ,  T tx x ϕϕ ϕ ϕ ψϕψψχχ ϕ ϕ ϕψ ϕψ ϕψ ϕψ ϕψ ϕ ϕ ¬ ∧ ∨ → ∀ ∆¬Γ ⇒∆Γ ΓΓ∆Γ⇒∆ Γ ∆ ΓΓ⇒∆ΓΓ ∆Γ⇒∆ Γ ∆∧Γ⇒∆ Γ ∆Γ⇒∆ Γ∆Γ⇒∆ Γ ∆∨Γ⇒∆ Γ ∆¬Γ⇒∆ Γ ∆Γ⇒∆Γ ∆→Γ⇒∆ Γ ∆Γ⇒∆ Γ ∆ ∀Γ⇒∆ Γ A R R R R R where in means that occurs in the proof tree of from and and in is a term, and is free in for . Definition 2.1. is an Rtheorem, denoted by if there is a sequence such that (i) = , nnnn ′′ ′′ ∆ Γ⇒∆Γ∆Γ⇒∆Γ (ii) for each either is an axiom, or is deduced by some Rrule of form 11 11   ii ii ii 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 Rcalculus). For any theories , ΓΓ and if and only if Theorem 2.4. The Rrules preserve the strong validity. Let be the logical language of the propositional logic. A literal is an atomic formula or the negation of an atomic formula; a clause is the disjunction of finitely many literals, and a theory is the conjunction of finitely many clauses. Definition 2.5. Given a theory a theory is a subtheory of denote d by if either or (i) if then (ii) if then either or and (iii) if then either or Let Then, and ,, ().ppqpp pqt ′ ′′′ ∧ ∧∧∨ Definition 2.6. Given a theory where is an occurrence of in a theory 1 = [,...,]= [/,...,/], n s ttss λλλ λ where the occurrence is replaced by the empty theory is called a pseu dosubtheory of denoted by Let Then, ,,,, ().pqpqp pqpppqt ′′′ ′′′ ∨∨∧∧∧∨ Proposit ion 2.7. For any theories and 2 ,s (i) implies and (ii) and imply and Proposition 2.8. For any theories and if then Proof. By the induction on the structure of Proposition 2.9. and are partial orderings on the set of all the theories. Given a theory let be the set of all the pseu dosubtheories of Each is determined by a set where each is an occurrence of in such that 1 = ([]/,...,[]/). n s tpp λλ Given any define 121 2 121 2 = max{:,}; = min{:,}. s ssssss s ssssss Proposit ion 2.10. For any pseudosubtheories and exist. Let be the lattice with the greatest element and the least element Proposit ion 2.11. For any pseudosubtheories if and only if More over, 121 2 121 2 ()=()(); ()=()(). sss s sss s τ ττ τ ττ ∪ ∩
One Sound and Complete RCalculus with PseudoSubtheory Minimal Change Property Copyright © 2013 SciRes. JCC 3. The RCalculus N The deduct ion system N: 12 11 1 212 1 122 121 2 () () , , , ()  ,  ,, () , aa ll NN ll l ts Nt tst c dcd Ncc dd λ ∧ ∨ ∆¬ ∆¬ ∆ ⇒∆∆ ⇒∆ ∆ ⇒∆ ∆∧ ⇒∆ ∆⇒∆ ∆⇒∆ ∆∨⇒∆∨ where denotes a theory is the empty string, and if is consistent then , sss sss λλ λλ λ ∨≡∨ ≡ ∧≡∧ ≡ ∆ ≡∆ and if is inconsistent then Definition 3.1. is Nprovable if there is a statement sequence }1:,{ nist iiii ≤≤∆⇒∆ such that and for each is either by an  rule or by an ,or rule. An exam pl e is the follo w i ng deduction for 11 1 1 212 1 121212 12 112 12 212 12 1212 112121212 12  ,  ,, , , , , , ,  ,, ,. ll l l lll l llllll ll lll ll lll ll llll lllll llll ll λ ¬ ⇒¬ ¬ ⇒¬ ¬∨⇒ ¬∨≡¬ ¬ ⇒¬ ¬ ¬⇒¬ ¬∨ ¬⇒¬ ¬∨∨¬⇒ ¬∨¬ ⇒¬ Notice that and Theorem 3.2. For any theory set and theory there is a theory such that is Nprova ble. Proof. We prove the theorem by the induction on the structure of If is a literal then either or If then and if then and If then by the induction assumption, there are theories s1, s2 such that and Therefore, and If then by the induction assumption, there are theories such that and Therefore, and Proposition 3.3. If is Nprovable then Proof. We prove the proposition by the induction on the length of the proof of If the last rule used is then and If the last rule used is then and If the last rule used is then and By the induction assumption, and Hence, If the last rule used is then and By the induction assumption, and Hence, Proposition 3.4. If is Nprovable then is consistent. Proof. We prove the proposition by the induction on the length of the proof of If the last rule used is then and Then, is consistent; If the last rule used is then and Then, is consistent; If the last rule used is then and By the induction assumption, and is consistent, and so is If the last rule used is then and By the induction assumption, and is consistent, and so is 4. The Completeness of the RCalculus N For any theory , def ine as follows: 1 12 12 1 212 if= and if= and (, )=(,) ({(,)},) if = (,)(,)if = tl l ltl l st st sstt tt t st stttt λ ∆¬ ∆¬ ∆∆ ∧∆∆ ∧ ∆ ∨∆∨ ∪ About the inconsistence, we have the following facts: • if then is inconsistent; • is inconsistent if and only if either is inconsistent or is in con sistent; • is inconsistent if and only if both and are inconsistent.
One Sound and Complete RCalculus with PseudoSubtheory Minimal Change Property Copyright © 2013 SciRes. JCC Proposition 4.1. For any consistent th eory set and a theory is consistent. Proof. We prove the proposition by the induction on the structure of If and l is consistent with then is consistent with if and is inconsistent with then is consistent with If then by the induction assumption, and 1 12 { (,),({(,)},)}sts stt∆∆ ∆∆∪∪ are consistent, so is consistent; If then by the induction assumption, and are consistent, so 121 2 {(,)}={(, )(,)}sccsc sc∆∆∨ ∆∆∨∆∪∪ is consis tent. About the consistence, we have the following facts: • if then is consistent; • is consistent if and only if is consistent and is consistent; • is consistent if and only if either or is consistent. Theorem 4.2. If is consistent then and Proof. We prove the theorem by the induction on the structure of If and is consistent with then and the theorem holds for If then and is con sistent, and by the induction assumption, 11 11 121 2 12 2 , (,) ,(,) ; ,,({ },) , ({ },), t st st t stss t s stt ∆∆ ∆∆ ∆∆ ∆∆ ∪ ∪ where Henc e, 1 2112 1121 2 ,( ,)({ },) , (,)({},). t tstsst stsstt t ∆ ∧∆∧∆ ∆ ∆∧∆∧ ∪ ∪ If then either or is consistent, and by the induction assumption, either 11 11 ,(, ) ,(, ); c sc sc c ∆∆ ∆∆ or 22 22 ,(, ) ,(, ). c sc scc ∆∆ ∆∆ Hence, we have 121 2 12 12 ,(, )(,) ,(, )(,). ccsc sc sc sccc ∆ ∨∆∨∆ ∆ ∆∨∆∨ Theorem 4.3. is Nprovable if and only if Proof. Assume that is Nprovable. We assume that for any the claim holds. If and the last rule is then and It is clear that If and the last rule is then and It is clear that If and the last rule is then and 121212 , ,,.ttstss∆∧ ⇒∆⇒∆ By the induction assumption, and Then, 1211212 ==(,) ({},)=(,);sssstsststt∧∆∧∆∆ ∧∪ If and the last rule is then and By the induction assumption, and 12 1212 ==(,)(,)=(,).ssssc scscc∨∆∨∆∆ ∨ Let We prove that is Nprovable by the induction on the structure of If and then and i.e., If and then and i.e., If then 1211 2 (,)=(,) ({(,)},).sttst sstt∆ ∧∆∧∆∆∪ By the induc tion assumption, and 12112 ,,,({ (,)},).s tssstt∆⇒∆∆ ∆∪ Therefore, 1211 2 ,,({ (,)},);t tssstt∆∧ ⇒∆∆∆∪ If then 1211 2 (,)=(, )({(, )},).sccsc sscc∆ ∨∆∨∆∆∪ By the in duction assumption, and Therefore, 121 2 ,(, )(,).ccscsc∆∨⇒∆∆∨ ∆ 5. The Logical Properties of t and It is clear that we have the following Proposit ion 5.1. For any theory set and theory Theorem 5.2. For any theory set and theory ,( ,)(,); ,( ,)( ,). t st st t ξ ξ ∆∆ ∆ ∆∆ ∆ Proof. By the definitions of and the induction on the structure of Proposition 5.3. (i) If then is in consistent; (ii) If then is consistent. Define = {():{}isconsistent}; = {():{}isinconsistent}. t t CsPts IsPts ∆ ∆ ∈∆ ∈∆ ∪ ∪ Then, and Define an equivalence relation on such that for any
One Sound and Complete RCalculus with PseudoSubtheory Minimal Change Property Copyright © 2013 SciRes. JCC Given a pseudosubtheory let be the equivalence class of Then, we ha ve that [ (, )],[(, )]. t sttC ξ ∆ ∆ ∆⊆ Proposit ion 5.4. Define a relation on such that for any and iff 12112 2 11 22 122111 21 1222 111 1222122 11 22122111211222 1111222122 =if == =&= or=&= if =and= =&= or=&= if=and = llsland sl cccc cccc sc cscc ssss ssss ss ssss ∨∨ ∧∧ Proposition 5.5. is an equivalence relation on and for any if then Theorem 5.6. If is provable then for any with is prova ble. Proof. We prove the theorem by the induction on the structure of If and then and for any with and is prova ble; If and then and for any with and is prova ble; If and the theorem holds for both and then and for any with there are and such that and By the induction assumption, 111 212 ,,, ,,,ssss ηη ∆⇒∆ ∆⇒∆ and by , 12121 2 ,, , ;sss s ηη ∆∧⇒∆≡∆ ∧ If and the theorem holds for both and then and for any with there are and such that and By the induction assumption, and by , Theorem 5.7. For any with if is consistent then and hence, and if is inconsistent then and hence, Proof. If is consistent then by Theorem 6.6, and we prove by the induction on the structure of that If and then and If and the claim holds for both and then and There fore, If and the theorem holds for both and then and there are three cases: Case 1. and are consistent. By the in duction a s s umption , we ha ve that 1 122 ,, ,,,,c dcd∆ ∆∆∆ and hence, Case 2. is consistent and is inconsistent. By the induction assumption, we have that and Then, 1 12 1 12 ,, ; d dd c cc ∆≡∆ ∨ ∨ and 1212 1 1112 ,( )() ,, ccc c c cddd ∆∨≡∆∧∨ ∆∧ ≡ ∆∧ ≡∆ ∨ where Case 3. Similar to Case 2. Corollary 5.8. For any with either or Therefore, is maximal such that is consistent. 6. Conclusions and Further Works We defined an Rcalculus N in propositional logic pro grams such that N is sound and complete with respect to the operator 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 and then It is not true in N that (*) if and then A further work is to give an Rcalculus having the property . A simplified form of is (**) if and then which is not true in N either. Another further work is to give an Rcalculus having the property and havin g not the property . REFERENCES [1] W. Li, “RCalculus: An Inference System for Belief Re vision,” The Computer Journal, Vol. 50, 2007, pp. 378 390. http://dx.doi.org/10.1093/comjnl/bxl069 [2] 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. 510530. http://dx.doi.org/10.2307/2274239 [3] A. Bochman, “A Foundational Theory of Belief and Be lief Change,” Artificial Intelligence, Vol. 108, 1999, pp. 309352. http://dx.doi.org/10.1016/S00043702(98)00112X [4] M. Dalal, “Investigations into a Theory of Knowledge
One Sound and Complete RCalculus with PseudoSubtheory Minimal Change Property Copyright © 2013 SciRes. JCC Base Revision: Preliminary Report,” Proceedings of AAAI88, St. Paul, 1988, pp. 475479. [5] 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. 35132. [6] A. Darwiche and J. Pearl, “On the Logic of Iterated Belief Revision,” Artificial Intelligence, Vol. 89, 1997, pp. 129. http://dx.doi.org/10.1016/S00043702(96)000380 [7] 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. 295331. http://dx.doi.org/10.1007/s1099201191719 [8] 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. 421431. [9] S. O. Hansson, “Theory Contraction and Base Contrac tion Unified,” Journal of Symbolic Logic, Vol. 58, 1993, pp. 602626. http://dx.doi.org/10.2307/2275221 [10] A. Herzig and O. Rifi, “Propositional Belief Base Update and Minimal Change,” Artificial Intelligence, Vol. 115, 1999, pp. 107138. http://dx.doi.org/10.1016/S00043702(99)000727 [11] K. Satoh, “Nonmonotonic Reasoning by Minimal Belief Revision,” Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, 1988, pp. 455462.
