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)
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.
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 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 ([1]) 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
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 ([1]) 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 22
12 12
( ),|,,|
,,|, |
() |, ,|,
|, |
() |, |
|,||,|
() |, |
|,||,|
() |,|
|[ /],|
() |, |
T
tx
x
ϕϕ ϕ
ϕ ψϕψψχχ
ϕ
ϕ
ϕψ
ϕψ
ϕψ
ϕψ
ϕψ
ϕ
ϕ
¬
∧
∨
→
∀
∆¬Γ ⇒∆Γ
ΓΓ∆Γ⇒∆ Γ
∆ ΓΓ⇒∆ΓΓ
∆Γ⇒∆ Γ
∆∧Γ⇒∆ Γ
∆Γ⇒∆ Γ∆Γ⇒∆ Γ
∆∨Γ⇒∆ Γ
∆¬Γ⇒∆ Γ ∆Γ⇒∆Γ
∆→Γ⇒∆ Γ
∆Γ⇒∆ Γ
∆ ∀Γ⇒∆ Γ

A
R
R
R
R
R

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 i
in
′′
∆Γ∆ Γ≤
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 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 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
1
st
or
2
;st
and
(iii) if
12
=tcc∨
then either
1
sc
or
2
.sc
Let
= ()().tpqp q
′′
∨∧ ∨
Then,
,;p qpqt
′′
∨∨
and
,, ().ppqpp pqt
′ ′′′
∧ ∧∧∨
Definition 2.6. Given a theory
1
[ ,...,],
n
tss
where
1
s
is an occurrence of
1
s
in
,t
a theory
1
= [,...,]= [/,...,/],
n
s ttss λλλ λ
where the occurrence
i
s
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)
11
st
implies
1 12
s tt∨
and
1 12
;s tt∧
(ii)
11
st
and
22
st
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
()= {[],...,[]},
n
sp p τ
where each
[]
i
p
is an
occurrence of
i
p
in
,t
such that
1
= ([]/,...,[]/).
n
s tpp λλ
Given any
12
,(),s sPt∈
define
121 2
121 2
= max{:,};
= min{:,}.
s ssssss
s ssssss
 
 
Proposit ion 2.10. For any pseudo-subtheories
121 2
,(),s sPtss∈
and
12
ss
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 2
121 2
()=()();
()=()().
sss s
sss s
τ ττ
τ ττ


∪
∩

One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property
22
3. The R-Calculus 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
,t∆
denotes a theory
{ };t λ ∆∪
is the empty
string, and if
s
is consistent then
,
sss
sss
λλ
λλ
λ
∨≡∨ ≡
∧≡∧ ≡
∆ ≡∆
and if
s
is inconsistent then
ss
ss
λ λλ
λ λλ
∨≡∨ ≡
∧≡∧ ≡
Definition 3.1.
|,ts∆ ⇒∆
is N-provable if there is a
statement sequence }1:,|{ nist
iiii
≤≤∆⇒∆
such that
|,= |,,
nn nn
ts ts∆ ⇒∆∆⇒∆
and for each
,in≤
|,
ii ii
ts∆ ⇒∆
is either by an
a
N
-
rule or by an
N
∧
-,or
N∨
-rule.
An exam pl e is the follo w i ng deduction for
1 1212
|, :lllll¬ ∨∨¬
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
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
()
a
N
then
=,tl
and
= =;sltl
If the last rule used is
2
()
a
N
then
=,tl
and
= =;s tl λ 
If the last rule used is
()N
∧
then
11
|,ts∆⇒∆
and
12 12
, |,,.s tss∆ ⇒∆
By the induction assumption,
11
st
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,
11
st
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
()
a
N
then
,l∆¬
and
| ,.ll∆ ⇒∆
Then,
{}l∆∪
is consistent;
If the last rule used is
2
()
a
N
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 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
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
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,
11
11
121 2
12 2
, (,)
,(,) ;
,,({ },)
, ({ },),
t st
st t
stss t
s stt
∆∆
∆∆
∆∆
∆∆
∪
∪




where
11
=( ,).sst∆
Henc e,
1 2112
1121 2
,( ,)({ },)
, (,)({},).
t tstsst
stsstt t
∆ ∧∆∧∆
∆ ∆∧∆∧
∪
∪


If
12
=tcc∨
then either
1
{}c∆∪
or
12
{, }cc∆∪
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.
|,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
()
a
N
then
l∆¬
and
| ,.ll∆ ⇒∆
It is clear that
==(, );sls l∆
If
=tl
and the last rule is
2
()
a
N
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 st
st 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}.
t
t
CsPts
IsPts
∆
∆
∈∆
∈∆
∪
∪
Then,
= ()
tt
C IPt
∆∆
∪
and
=.
tt
CI
∆∆
∅∩
Define an equivalence relation
∆
≡
on
()tP
such
that for any
12
,(),s sPt∈
121 2
iff,, .sss s
∆
≡ ∆∆

One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property
24
Given a pseudo-subtheory
( ),s Pt∈
let
[]r
be the
equivalence class of
.s
Then, we ha ve that
[ (, )],[(, )].
t
sttC ξ
∆
∆ ∆⊆
Proposit ion 5.4.
[(, )]=[(, )].st t
ξ ∆∆
Define a relation

on
)(tP
such that for any
1
s
and
2 12
( ),sPt ss∈
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
( ),Pt
and for any
12
,(),s sPt∈
if
12
ss
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
1
t
and
2
t
then
12
=,sss∧
and for any
η
with
,st η 
there are
1
η
and
2
η
such that
1 11
st η 
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
1
c
and
2
c
then
12
=,sss∨
and for any
η
with
,st η 
there are
1
η
and
2
η
such that
111
sc η 
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
1
t
and
2
t
then
12 11
= ,,,sss ts∧∆∆
and
22
, ,.ts∆∆
There-
fore,
1212
, ,.tt ss∆∧∆∧
If
21
=cct ∨
and the theorem holds for both
1
c
and
2
c
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 12
1
12
,,
;
d dd
c
cc
∆≡∆ ∨
∨


and
1212
1
1112
,( )()
,,
ccc c
c
cddd
∆∨≡∆∧∨ ∆∧
≡ ∆∧
≡∆ ∨
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
[1] 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
[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. 510-530.
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.
309-352.
http://dx.doi.org/10.1016/S0004-3702(98)00112-X
[4] M. Dalal, “Investigations into a Theory of Knowledge

One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property
25
Base Revision: Preliminary Report,” Proceedings of
AAAI-88, St. Paul, 1988, pp. 475-479.
[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. 35-132.
[6] 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
[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. 295-331.
http://dx.doi.org/10.1007/s10992-011-9171-9
[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. 421-431.
[9] 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
[10] 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
[11] K. Satoh, “Nonmonotonic Reasoning by Minimal Belief
Revision,” Proceedings of the International Conference
on Fifth Generation Computer Systems, Tokyo, 1988, pp.
455-462.