One Sound and Complete <i>R</i>-Calculus with Pseudo-Subtheory Minimal Change Property

doi:10.4236/jcc.2013.15004

Paper Menu >>

Journal Menu >>

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.

Email: [email protected], [email protected] 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 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

∆

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

-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

.∆

The

-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

is a theory in propositional logic

programs, such that

•

,( ,)st∆∆

is consistent;

•

( ,)st∆

is a pseudo-subt he o r y of

•

( ,)st∆

is maximal such that

,( ,)st∆∆

is consistent,

and for any pseudo-subtheory

( ,)st∆

a pseudo-subtheory of

and

is not a pseudo-

subtheory of

then either

,( ,)st

∆∆

and

,( ,),st

∆∆

∆

is inconsistent.

Then, we give one

-calculus N such that N is sound

and complete with respect to operator

(, ),st∆

where

 N is sound with respect to operator

(, ),st∆

|,ts∆ ⇒∆

being provable implies

=(, ),ss t∆

and

 N is complete with respect to operator

(, ),st∆

|,( ,)t st∆ ⇒∆∆

is prova ble.

Let



be the pseudo-subtheory relation,

()Pt

the set of all the pseudo-subtheories of

and

∆

≡

an equivalence relation on

()Pt

such that for any

121 2

,( ),Pt

ηηη η

∆

∈≡

iff

, ,.

ηη

∆∆

Given a

pseudo-subtheory



let

[]

be the equivalence

class of

with respect to

∆

≡

About the minimal change, we prove that

[(, )]st∆



-maximal in

( )/Pt

∆

≡

such that

,( ,)st∆∆

is con-

sistent, that is,

♦

,( ,)st∆∆

is consistent; and

♦ for any

such that

[(,)][] [],st t

∆

either

[][(, )]st

∆

∆

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

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

′ 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

( ),|,,|

,,|, |

() |, ,|,

|, |

() |, |

|,||,|

() |, |

|,||,|

() |,|

|[ /],|

() |, |

ϕϕ ϕ

ϕ ψϕψψχχ

ϕψ

∧

∨

→

∀

∆¬Γ ⇒∆Γ

ΓΓ∆Γ⇒∆ Γ

∆ ΓΓ⇒∆ΓΓ

∆Γ⇒∆ Γ

∆∧Γ⇒∆ Γ

∆Γ⇒∆ Γ∆Γ⇒∆ Γ

∆∨Γ⇒∆ Γ

∆¬Γ⇒∆ Γ ∆Γ⇒∆Γ

∆→Γ⇒∆ Γ

∆Γ⇒∆ Γ

∆ ∀Γ⇒∆ Γ





where in

cut ,T

ϕψ

R

means that

occurs in the

proof tree

from

and

;

and in

,Rt

∀

a term, and is free in

for

Definition 2.1.

′′

∆ Γ⇒∆Γ

is an R-theorem,

denoted by

| |,

′′

∆ Γ⇒∆Γ

if there is a sequence

{( ,,,):}

iii i

′′

∆Γ∆ Γ≤

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

−− −−

′′

∆Γ⇒∆Γ

′′

∆Γ⇒∆Γ

Definition 2.2.

′

∆Γ⇒∆Γ

is valid, denoted by

| |,

′

∆Γ⇒∆Γ

if for any contraction

of ′

Γ by

,∆Θ

is a contraction of

.∆

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

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

sub-theory of

denote d by

,st

if either

=,ts

(i) if

=tt¬

then

;st

(ii) if

=ttt ∧

then either

st

;st

and

(iii) if

=tcc∨

then either

sc

.sc

Let

= ()().tpqp q

′′

∨∧ ∨

Then,

,;p qpqt

′′

∨∨

and

,, ().ppqpp pqt

′ ′′′

∧ ∧∧∨

Definition 2.6. Given a theory

[ ,...,],

tss

where

is an occurrence of

a theory

= [,...,]= [/,...,/],

s ttss

λλλ λ

where the occurrence

is replaced by the empty theory

is called a pseu-

do-subtheory of

denoted by

.st

Let

= ()().tpqp q

′′

∨∧ ∨

Then,

,,,, ().pqpqp pqpppqt

′′′ ′′′

∨∨∧∧∧∨

Proposit ion 2.7. For any theories

12 1

,,tts

and 2

(i)

st

implies

1 12

s tt∨

and

1 12

;s tt∧

(ii)

st

and

st

imply

11121 2

,stsstt¬¬∨ ∨

and

1 212

.ss tt∧∧

Proposition 2.8. For any theories

and

st

then

.st

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

()Pt

be the set of all the pseu-

do-subtheories of

Each

()s Pt∈

is determined by a

set

()= {[],...,[]},

sp p

where each

[]

is an

occurrence of

such that

= ([]/,...,[]/).

s tpp

λλ

Given any

,(),s sPt∈

define

121 2

= max{:,};

= min{:,}.

s ssssss

 

 

Proposit ion 2.10. For any pseudo-subtheories

121 2

,(),s sPtss∈

and

ss

exist.

Let

()=((), ,,, )Pt Ptt



be the lattice with the

greatest element

and the least element

Proposit ion 2.11. For any pseudo-subtheories

121 2

,(),s sPtss∈

if and only if

( )().ss

ττ

⊇

More-

over,

121 2

()=()();

()=()().

sss s

τ ττ





∪

∩

One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property

3. The R-Calculus N

The deduct ion system N:

1 212

1 122

121 2

() ()

|, |,

()

| ,|

| ,|,

() |,

ll l

Nt tst

c dcd

Ncc dd

∧

∨

∆¬ ∆¬

∆ ⇒∆∆ ⇒∆

∆ ⇒∆

∆∧ ⇒∆

∆⇒∆ ∆⇒∆

∆∨⇒∆∨



where

,t∆

denotes a theory

{ };t

∆∪

is the empty

string, and if

is consistent then

sss

λλ

∨≡∨ ≡

∧≡∧ ≡

∆ ≡∆

and if

is inconsistent then

λ λλ

∨≡∨ ≡

∧≡∧ ≡

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

rule or by an

∧

-,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

| ,,

,| ,

| ,,|

ll l

l lll

l llllll

ll lll

ll llll

lllll llll

¬ ⇒¬

¬∨⇒ ¬∨≡¬

¬ ⇒¬

¬ ¬⇒¬

¬∨ ¬⇒¬

¬∨∨¬⇒ ¬∨¬

⇒¬

Notice that

11 1

|ll l¬ ⇒¬

and

1 1212

() ().l llll≡∨∧∨¬

Theorem 3.2. For any theory set

∆

and theory

there is a theory

such that

|,ts∆ ⇒∆

is N-prova-

ble.

Proof. We prove the theorem by the induction on the

structure of

=tl

is a literal then either

l∆¬

.l∆¬

l∆¬

then

|,l

∆ ⇒∆

and

=;s

l∆¬

then

|,ll∆ ⇒∆

and

=;sl

=ttt∧

then by the induction assumption, there

are theories s1, s2 such that

|,ts∆ ⇒∆

and

12 12

, |,,.s tss∆ ⇒∆

Therefore,

1 212

| ,,t tss∆∧ ⇒∆

and

=.sss∧

=tcc∨

then by the induction assumption, there

are theories

,ss

such that

|,cs∆ ⇒∆

and

| ,.cs∆ ⇒∆

Therefore,

12 12

|,cc ss∆∨ ⇒∆∨

and

=.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

()

then

=,tl

and

= =;sltl

If the last rule used is

()

then

=,tl

and

= =;s tl



If the last rule used is

()N

∧

then

|,ts∆⇒∆

and

12 12

, |,,.s tss∆ ⇒∆

By the induction assumption,

st

and

.st

Hence,

1 212

=;sstt t∧∧

If the last rule used is

()N

∧

then

|,cs∆ ⇒∆

and

| ,.cs∆ ⇒∆

By the induction assumption,

st

and

.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

()

then

,l∆¬

and

| ,.ll∆ ⇒∆

Then,

{}l∆∪

is consistent;

If the last rule used is

()

then

,l∆¬

and

| ,.l

∆ ⇒∆

Then,

{}

∆∪

is consistent;

If the last rule used is

()N

∧

then

|,ts∆⇒∆

and

12 12

, |,,.s tss∆ ⇒∆

By the induction assumption,

{}s∆∪

and

{, }ss∆∪

is consistent, and so is

{}={};ss s∆∧ ∆∪∪

If the last rule used is

()N

∨

then

|,cs∆ ⇒∆

and

| ,.cs∆ ⇒∆

By the induction assumption,

{}s∆∪

and

{}s∆∪

is consistent, and so is

{}={}.ss s∆∨ ∆∪∪

4. The Completeness of the R-Calculus N

For any theory

, def ine

( ,)st∆

as follows:

1 12

1 212

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;

•

{}tt∆∧∪

is inconsistent if and only if either

{}t∆∪

is inconsistent or

{, }tt∆∪

is in- con-

sistent;

•

{}cc∆∨∪

is inconsistent if and only if both

{}c∆∪

and

{}c∆∪

are inconsistent.

One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property

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

=tl

and l is consistent with

∆

then

(, )=sll∆

is consistent with

;∆

=tl

and

is inconsistent

with

∆

then

(, )=sl

∆

is consistent with

;∆

=ttt∧

then by the induction assumption,

{ (,)}st∆∆∪

and

1 12

{ (,),({(,)},)}sts stt∆∆ ∆∆∪∪

are

consistent, so

{ (,)}stt∆ ∆∧∪

is consistent;

=tcc∨

then by the induction assumption,

{ (,)}sc∆∆∪

and

{ (,)}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;

•

{}tt∆∧∪

is consistent if and only if

{}t∆∪

consistent and

{, }tt∆∪

is consistent;

•

{}cc∆∨∪

is consistent if and only if either

{}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

=tl

and

is consistent with

∆

then

(, )=,sll∆

and the theorem holds for

=ttt∧

then

{}t∆∪

and

{, }tt∆∪

is con-

sistent, and by the induction assumption,

121 2

12 2

, (,)

,(,) ;

,,({ },)

, ({ },),

t st

st t

stss t

s stt

∆∆

∪



where

=( ,).sst∆

Henc e,

1 2112

1121 2

,( ,)({ },)

, (,)({},).

t tstsst

stsstt t

∆ ∧∆∧∆

∆ ∆∧∆∧

∪



=tcc∨

then either

{}c∆∪

{, }cc∆∪

consistent, and by the induction assumption, either

,(, )

,(, );

c sc

sc c

∆∆



,(, )

,(, ).

c sc

scc

∆∆



Hence, we have

121 2

12 12

,(, )(,)

,(, )(,).

ccsc sc

sc sccc

∆ ∨∆∨∆

∆ ∆∨∆∨



Theorem 4.3.

|,ts∆ ⇒∆

is N-provable if and only

=(, ).ss t∆

Proof.

()⇒

Assume that

|,ts∆ ⇒∆

is N-provable.

We assume that for any

<,in

the claim holds.

=tl

and the last rule is

()

then

l∆¬

and

| ,.ll∆ ⇒∆

It is clear that

==(, );sls l∆

=tl

and the last rule is

()

then

l∆¬

and

| ,.l

∆ ⇒∆

It is clear that

==(, );ssl

∆

=ttt∧

and the last rule is

()N

∧

then

|,ts∆⇒∆

and

121212

|, |,,.ttstss∆∧ ⇒∆⇒∆

the induction assumption,

( ,)=st s∆

and

12 2

({},) =.sst s∆∪

Then,

1211212

==(,) ({},)=(,);sssstsststt∧∆∧∆∆ ∧∪

=tcc∨

and the last rule is

()N

∨

then

|,cs∆ ⇒∆

and

| ,.cs∆ ⇒∆

By the induction

assumption,

1 122

=( ,),=(,),sscssc∆∆

and

12 1212

==(,)(,)=(,).ssssc scscc∨∆∨∆∆ ∨

()⇐

Let

=(, ).ss t∆

We prove that

|,ts∆ ⇒∆

N-provable by the induction on the structure of

=tl

and

l∆¬

then

(, )=,sl

∆

and

| ,,l

∆ ⇒∆

i.e.,

| ,;ls∆ ⇒∆

=tl

and

l∆¬

then

(, )=,sll∆

and

| ,,ll∆ ⇒∆

i.e.,

| ,;ls∆ ⇒∆

=ttt∧

then

1211 2

(,)=(,) ({(,)},).sttst sstt∆ ∧∆∧∆∆∪

By the induc-

tion assumption,

| ,(,)t st∆⇒∆ ∆

and

12112

,|,,({ (,)},).s tssstt∆⇒∆∆ ∆∪

Therefore,

1211 2

|,,({ (,)},);t tssstt∆∧ ⇒∆∆∆∪

=tcc∨

then

1211 2

(,)=(, )({(, )},).sccsc sscc∆ ∨∆∨∆∆∪

By the in-

duction assumption,

|,(, )c sc∆⇒∆ ∆

and

|, (,).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

( ,)(,).tst

∆∆

Theorem 5.2. For any theory set

∆

and theory

,( ,)(,);

,( ,)( ,).

t st

st t

∆∆ ∆



Proof. By the definitions of

(,),(,)st

ξξ

∆∆

and the

induction on the structure of

Proposition 5.3. (i) If

,( ,)stt∆∆ 

then

,t∆

is in-

consistent;

(ii) If

,( ,)stt∆∆

then

,t∆

is consistent.

Define

= {():{}isconsistent};

= {():{}isinconsistent}.

CsPts

IsPts

∆

∈∆

∪

Then,

= ()

C IPt

∆∆

∪

and

∆∆

∅∩

Define an equivalence relation

∆

≡

()tP

such

that for any

,(),s sPt∈

121 2

iff,, .sss s

∆

≡ ∆∆

One Sound and Complete R-Calculus with Pseudo-Subtheory Minimal Change Property

Given a pseudo-subtheory

( ),s Pt∈

let

[]r

be the

equivalence class of

Then, we ha ve that

[ (, )],[(, )].

sttC

∆

∆ ∆⊆

Proposit ion 5.4.

[(, )]=[(, )].st t

∆∆

Define a relation



)(tP

such that for any

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

,(),s sPt∈

ss

then

.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

=tl

and

l∆¬

then

=,s

and for any

with

,=,st

η ηλ



and

ηλ

∆ ⇒∆

is prova ble;

=tl

and

l∆¬

then

=,sl

and for any

with

, =,s tl

ηη



and

|,s

∆ ⇒∆

is prova ble;

=ttt∧

and the theorem holds for both

and

then

=,sss∧

and for any

with

,st



there are

and

such that

1 11



and

2 22

.st



By the induction assumption,

111 212

|,,, |,,,ssss

ηη

∆⇒∆ ∆⇒∆

and by

()N∧

12121 2

|,, , ;sss s

ηη

∆∧⇒∆≡∆ ∧

=tcc∨

and the theorem holds for both

and

then

=,sss∨

and for any

with

,st



there are

and

such that

111



and

222

.sc



By the induction assumption,

1 122

| ,;|,,ss

ηη

∆⇒∆ ∆⇒∆

and by

()N∨

1 212

| ,.ss

ηη

∆∨⇒∆ ∨

Theorem 5.7. For any

with

,st



∆

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

that

, ,.ts∆∆

=tl

and

l∆¬

then

=,sl

and

, ,;ts∆∆

=ttt∧

and the claim holds for both

and

then

12 11

= ,,,sss ts∧∆∆

and

, ,.ts∆∆

There-

fore,

1212

, ,.tt ss∆∧∆∧

=cct ∨

and the theorem holds for both

and

then

=,ddd∨

and there are three cases:

Case 1.

,c∆

and

,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.

,c∆

is consistent and

,c∆

is inconsistent.

By the induction assumption, we have that

, ,,cd∆∆

and

|.c∆ ⇒∆

Then,

1 12

;

d dd

∆≡∆ ∨

∨



and

1212

1112

,( )()

ccc c

cddd

∆∨≡∆∧∨ ∆∧

≡ ∆∧

≡∆ ∨

where

=.d

Case 3. Similar to Case 2.

Corollary 5.8. For any

with

,st



either

][=][ s

[] = [].t

Therefore,

[]s



-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

.ss

It is not true in N that

(*) if

1 211

;| ,sststs

′

⇒

and

|,tsts

′

⇒

then

.ss

′′



A further work is to give an R-calculus having the

property

()∗

A simplified form of

()∗

(**) if

121 1

;| ,sststs

′

⇒

and

|,tsts

′

⇒

then

,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

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.