Annotated revision programs.
Revision programming is a formalism to describe and enforce updates of belief sets and databases. That formalism was extended by Fitting who assigned annotations to revision atoms. Annotations provide a way to quantify the confidence (probability) that a revision atom holds. The main goal of our paper is to reexamine the work of Fitting, argue that his semantics does not always provide results consistent with intuition, and to propose an alternative treatment of annotated revision programs. Our approach differs from that proposed by Fitting in two key aspects: we change the notion of a model of a program and we change the notion of a justified revision. We show that under this new approach fundamental properties of justified revisions of standard revision programs extend to the annotated case.
Introduction
Revision programming is a formalism to specify and enforce constraints on
databases, belief sets and, more generally, on arbitrary sets of elements. Revision
programming was introduced and studied in [MT95,MT98]. The formalism was
shown to be closely related to logic programming with stable model semantics
[MT98,PT97]. In [MPT99], a simple correspondence of revision programming
with the general logic programming system of Lifschitz and Woo [LW92] was dis-
covered. Roots of another recent formalism of dynamic programming [ALP
can also be traced back to revision programming.
Revision rules come in two forms of in-rules and out-rules:
in(a)
and
out(a)
Expressions in(a) and out(a) are called revision atoms. Informally, the atom
in(a) stands for "a is in the current set" and out(a) stands for "a is not in the
current set." The rules (1) and (2) have the following imperative, or computa-
tional, interpretation: whenever elements a k , 1 - k - m, belong to the current
set (database, belief set) and none of the elements belongs to the
current set then, in the case of rule (1), the item a must be added to the set (if it
is not there already), and in the case of rule (2), a must be eliminated from the
database (if it is there). The rules (1) and (2) have also an obvious declarative
interpretation.
To provide a precise semantics to revision programs, that is, collections of
revision rules, the concept of a justified revision was introduced in [MT95,MT98].
Informally, given an initial set B I and a revision program P , a justified revision
of B I with respect to P (or, simply, a P -justified revision of B I ) is obtained
from B I by adding some elements to B I and by removing some other elements
from B I so that each change is, in a certain sense, justified by the program.
The formalism of revision programs was extended by Fitting [Fit95] to the
case when revision atoms are assigned annotations. These annotations can be
interpreted as the degree of confidence that a revision atom holds. For instance,
an annotated atom (in(a):0:2) can be regarded as the statement that a is in the
set with probability 0:2. In his paper, Fitting described the concept of a justified
revision of an annotated program and studied properties of that notion.
The main goal of our paper is to reexamine the work of Fitting, argue that
his semantics does not always provide results consistent with intuition, and to
propose an alternative treatment of annotated revision programs. Our approach
differs from that proposed by Fitting in two key aspects: we change the notion of
a model of a program and we change the notion of a justified revision. We show
that under this new approach all fundamental properties of justified revisions of
standard revision programs extend to the case of annotated revision programs.
We also show that annotated revision programming can be given a more uniform
treatment if the syntax of revision programs is somewhat modified. The
new syntax yields a formalism that is equivalent to the original formalism of
annotated revision programs. The advantage of the new syntax is that it allows
us to generalize the shifting theorem proved in [MPT99] and used there to establish
the equivalence of revision programming with general logic programming
of Lifschitz and Woo [LW92].
Finally, in the paper we also address briefly the issue of disjunctive annotated
programs and other possible research directions.
Preliminaries
Throughout the paper we consider a fixed universe U whose elements are referred
to as atoms. Expressions of the form in(a) and out(a), where a 2 U , are called
revision atoms. In the paper we assign annotations to revision atoms. These
annotations are members of a complete distributive lattice with the de Morgan
complement (an order reversing involution). Throughout the paper this lattice is
denoted by T . The partial ordering on T is denoted by - and the corresponding
meet and join operations by - and -, respectively. The de Morgan complement
of a 2 T is denoted by - a.
An annotated revision atom is an expression of the form (in(a):ff) or (out(a):
ff), where a 2 U and ff 2 T . An annotated revision rule is an expression of the
where are annotated revision atoms. An annotated revision program
is a set of annotated revision rules.
A T -valuation is a mapping from the set of revision atoms to T . A T -
valuation v describes our information about the membership of the elements
from U in some (possibly unknown) set B ' U . For instance,
can be interpreted as saying that a 2 B with certainty ff. A T -valuation v
satisfies an annotated revision atom (in(a):ff) if v(in(a)) - ff. Similarly, v satisfies
ff. The T -valuation v satisfies a list or a set
of annotated revision atoms if it satisfies each member of the list or the set.
A T -valuation satisfies an annotated revision rule if it satisfies the head of the
rule whenever it satisfies the body of the rule. Finally, a T -valuation satisfies an
annotated revision program (is a model of the program) if it satisfies all rules in
the program.
Given a revision program P we can assign to it an operator on the set of all
-valuations. Let t P (v) be the set of the heads of all rules in P whose bodies
are satisfied by v. We define an operator TP as follows:
(note that ? is the join of an empty set of lattice elements). The operator
TP is a counterpart of the well-know van Emden-Kowalski operator from logic
programming and it will play an important role in our paper.
It is clear that under T -valuations, the information about an element a 2 U
is given by a pair of elements from T that are assigned to revision atoms in(a)
and out(a). Thus, in the paper we will also consider an algebraic structure T 2
with the domain T \Theta T and with an ordering - k defined by:
If a pair hff 1 viewed as a measure of our information about membership
of a in some unknown set B then ff 1 - ff 2 and fi 1 - fi 2 imply that the pair
higher degree of knowledge about a. Thus, the ordering - k
is often referred to as the knowledge or information ordering. Since the lattice
T is complete, T 2 is a complete lattice with respect to the ordering - k 1 .
The operations of meet, join, top, and bottom under - k are
?, and ?, respectively. In addition, we make use of an additional operation,
conflation. Conflation is defined as \Gammahff;
ffi. An element A 2 T 2 is
consistent if A - k \GammaA.
-valuation is a mapping from atoms to elements of T 2 . If
under some T 2 -valuation B, we say that under B the element a is in a set with
certainty ff and it is not in the set with certainty fi. We say that a T 2 -valuation
is consistent if it assigns a consistent element of T 2 to every atom in U .
1 There is another ordering that can be associated with T 2 . We can define hff
This ordering is often called the truth ordering.
Since T is a distributive lattice, T 2 with both orderings -k and - t forms a bilattice
(see [Gin88,Fit99] for a definition). In this paper we will not use the ordering - t nor
the fact that T 2 is a bilattice.
In the paper, T 2 -valuations will be used to represent current information
about sets (databases) as well as change that needs to be enforced. Let B be
a T 2 -valuation representing our knowledge about a certain set and let C be a
representing change that needs to be applied to B. We define the
by C by
The intuition is as follows. After the revision, the new valuation must contain
at least as much knowledge about atoms being in and out as C. On the other
hand, this amount of knowledge must not exceed implicit bounds present in
C and expressed by \GammaC , unless C directly implies so (if
evidence for in(a) must not exceed -
fi and the evidence for out(a) must not
exceed -
ff, unless C directly implies so). Since we prefer explicit evidence of C
to implicit evidence expressed by \GammaC , we perform the change by first using \GammaC
and then applying C (however, let us note here that the order matters only if
C is inconsistent; if C is consistent,
C)\Omega \GammaC ). This
specification of how a change modeled by a T 2 -valuation is enforced plays a key
role in our definition of justified revisions in Section 4.
There is a one-to-one correspondence ' between T -valuations (of revision
atoms) and T 2 -valuations (of atoms). For a T -valuation v, the T 2 -valuation
'(v) is defined v(out(a))i. The inverse mapping of ' is
denoted by ' \Gamma1 . Clearly, using the mapping ', the notions of satisfaction defined
earlier for T -valuations can be extended to T 2 -valuations. Similarly, the operator
TP gives rise to a related operator T b
. The operator T b
P is defined on the set of
all -valuations by T b
. The key property of the operator T b
P is
its - k -monotonicity.
Theorem 1. Let P be an annotated revision program and let B and B 0 be two
-valuations such that
By Tarski-Knaster Theorem it follows that the operator T b
P has a least fixpoint
in T 2 [KS92]. This fixpoint is an analogue of the concept of a least Herbrand
model of a Horn program. It represents the set of annotated revision atoms
that are implied by the program and, hence, must be satisfied by any revision
under P of any initial valuation. Given an annotated revision program P we
will refer to the least fixpoint of the operator T b
P as the necessary change of P
and will denote it by NC(P ). The present concept of the necessary change generalizes
the corresponding notion introduced in [MT95,MT98] for the original
unannotated revision programs.
To illustrate concepts and results of the paper, we will consider two special
lattices. The first of them is the lattice with the domain [0; 1] (interval of reals)
and with the standard ordering - and the standard complement operation. We
will denote this lattice by T [0;1] . Intuitively, the annotated revision atom (in(a):
x), where x 2 [0; 1], stands for the statement that a is "in" with likelihood
(certainty) x.
The second lattice is the Boolean algebra of all subsets of a given set X . It will
be denoted by TX . We will think of elements from X as experts. The annotated
revision atom (out(a):Y ), where Y ' X , will be understood as saying that a is
believed to be "out" by those experts that are in Y (the atom (in(a):Y ) has a
similar meaning).
3 Models and c-models
The semantics of annotated revision programs will be based on the notion of a
model as defined in the previous section. The following result provides a characterization
of the concept of a model in terms of the operator T b
Theorem 2. A T 2 -valuation B of an annotated revision program P is a model
of
Given an annotated revision program P , its necessary change NC(P ) satisfies
is a model of P .
As we will argue now, not all models are appropriate for describing the meaning
of an annotated revision program. The problem is that T 2 -valuations may
contain inconsistent information about elements from U . When studying the
meaning of an annotated revision program we will be interested in those models
only whose inconsistencies are limited by the information explicitly or implicitly
present in the program.
Consider the annotated revision program P , consisting of the following rule:
(in(a):fqg) / (out(a):fpg)
(the literals are annotated with elements of the lattice T fp;qg ). Some models of
this program are consistent (for instance, the T 2 -valuation that assigns hfqg; fpgi
to a). However, P also has inconsistent models. Let us consider first the T 2 -
valuation is a model of P . More-
over, it is an inconsistent model - the expert p believes both in(a) and out(a).
Let us notice though that this inconsistency is not disallowed by the program.
The rule (in(a) : fqg) / (out(a) : fpg) is applicable with respect to B 1 and,
thus, provides an explicit evidence that q believes in in(a). This fact implicitly
precludes q from believing in out(a). However, this rule does not preclude that
expert p believes in out(a). In addition, since no rule in the program provides
any information about out(a), it prevents neither p nor q from believing in in(a).
To summarize, the program allows for p to have inconsistent beliefs (however,
q's beliefs must be consistent).
Next, consider the
valuation is also a model of P . In B 2 both p and q are inconsistent in their
beliefs. As before, the inconsistent beliefs of p are not disallowed by P . However,
reasoning as before we see that the program disallows q to believe in out(a). Thus
the inconsistent beliefs of expert q cannot be reconciled with P . In our study of
annotated revision programs we will restrict ourselves only to consistent models
and to those inconsistent models whose all inconsistencies are not disallowed by
the program.
Speaking more formally, by direct (or explicit) evidence we mean evidence
provided by heads of program rules applicable with respect to B. It can be
described as T b
(B). The implicit bound on allowed annotations is given by a
version of the closed world assumption: if the evidence for a revision atom l
provided by the program is ff then, the evidence for the dual revision atom l D
(in(a), if l = out(a), or out(a), otherwise) must not exceed -
ff (unless explicitly
forced by the program). Thus, the implicit upper bound on allowed annotations
is given by \GammaT b
(B). Hence, a model B of a program P contains no more evidence
than what is implied by P given
P (B)). This
discussion leads us to a refinement of the notion of a model of an annotated
revision program.
Definition 1. Let P be an annotated revision program and let B be a T 2 -
valuation. We say B is a c-model of P if
Thus, coming back to our example, the T 2 -valuation B 1 is a c-model of P
and B 2 is not.
The "c" in the term c-model is to emphasize that c-models are "as consistent
as possible", that is, inconsistencies are limited to those that are not explicitly
or implicitly disallowed by the program. The notion of a c-model will play an
important consideration in our considerations.
Clearly, by Theorem 2, a c-model of P is a model of P . In addition, it is easy
to see that the necessary change of an annotated program P is a c-model of P
(it follows directly from the fact that NC(P
The distinction between models and c-models appears only in the context of
inconsistent information. This observation is formally stated below.
Theorem 3. Let P be an annotated revision program. A consistent T 2 -valu-
ation B is a c-model of P if and only if B is a model of P .
Justified revisions
In this section, we will extend to the case of annotated revision programs the
notion of a justified revision introduced for revision programs in [MT95]. The
reader is referred to [MT95,MT98] for the discussion of motivation and intuitions
behind the concept of a justified revision and of the role of the inertia principle
(a version of the closed world assumption).
There are several properties that one would expect to hold when the notion
of justified revision is extended to the case of programs with annotations.
Clearly, the extended concept should specialize to the original definition if annotations
can be dropped. Next, all main properties of justified revisions studied in
should have their counterparts in the case of justified revisions
of annotated programs. In particular, justified revisions of an annotated logic
program should satisfy it. Finally, there is one other requirement that naturally
arises in the context of programs with annotations.
Consider two annotated revision rules r and r 0 that are exactly the same
except that the body of r contains two annotated revision atoms l:fi 1 and l:fi 2 ,
while the body of r 0 instead of l:fi 1 and l:fi 2 contains annotated revision atom
It is clear, that for any T 2 -valuation B, B satisfies (l:fi 1 ) and (l:fi 2 ) if and only
Consequently, replacing rule r by rule r 0 (or vise versa)
in an annotated revision program should have no effect on justified revisions
In fact, any reasonable semantics for annotated revision programs should be
invariant under such operation, and we will refer to this property of a semantics
of annotated revision programs as invariance under join.
In this section we introduce the notion of the justified revision of an annotated
revision program and contrast it with an earlier proposal by Fitting [Fit95]. In
the following section we show that our concept of a justified revision satisfies all
the requirements listed above.
Let a T 2 -valuation B I represent our current knowledge about some subset of
the universe U . Let an annotated revision program P describe an update that
I should be subject to. The goal is to identify a class of T 2 -valuations that
could be viewed as representing updated information about the subset, obtained
by revising B I by P . As argued in [MT95,MT98], each appropriately "revised"
valuation BR must be grounded in P and in B I , that is, any difference between
I and the revised T 2 -valuation BR must be justified by means of the program
and the information available in B I .
To determine whether BR is grounded in B I and P , we use the reduct of P
with respect to the two valuations. The construction of reduct consists of two
steps and mirrors the original definition of the reduct of an unannotated revision
program [MT98]. In the first step, we eliminate from P all rules whose bodies
are not satisfied by BR (their use does not have an a posteriori justification with
respect to BR ). In the second step, we take into account the initial valuation B I .
How can we use the information about the initial T 2 -valuation B I at this
stage? Assume that B I provides evidence ff for a revision atom l. Assume also
that an annotated revision atom (l:fi) appears in the body of a rule r. In order
to satisfy this premise of the rule, it is enough to derive, from the program
resulting from step 1, an annotated revision atom (l:fl), where ff - fl - fi. The
least such element exists (due to the fact that T is complete and distributive).
Let us denote it by pcomp(ff; fi) 2 .
Thus, in order to incorporate information about a revision atom l contained
in the initial T 2 -valuation B I , which is given by I ))(l), we proceed
2 The operation pcomp(\Delta; \Delta) is known in the lattice theory as the relative pseudocom-
plement, see [RS70].
as follows. In the bodies of rules of the program obtained after step 1, we replace
each annotated revision atom of the form (l:fi) by the annotated revision atom
(l:pcomp(ff; fi)).
Now we are ready to formally introduce the notion of reduct of an annotated
revision program P with respect to the pair of T 2 -valuations, initial one, B I ,
and a candidate for a revised one, BR .
Definition 2. The reduct PBR jB I is obtained from P by
1. removing every rule whose body contains an annotated atom that is not satisfied
in BR ,
2. replacing each annotated atom (l:fi) from the body of each remaining rule by
the annotated atom (l:fl), where
We now define the concept of a justified revision. Given an annotated revision
program P , we first compute the reduct PBR jB I of the program P with respect
to B I and BR . Next, we compute the necessary change for the reduced program.
Finally we apply the change thus computed to the T 2 -valuation B I . A T 2 -
valuation BR is a justified revision of B I if the result of these three steps is BR .
Thus we have the following definition.
Definition 3. BR is a P -justified revision of B I if
I ) is the necessary change for PBR jB I .
We will now contrast the above approach with one proposed by Fitting in
[Fit95]. In order to do so, we recall the definitions introduced in [Fit95]. The key
difference is in the way Fitting defines the reduct of a program. The first step
is the same in both approaches. However, the second steps, in which the initial
valuation is used to simplify the bodies of the rules not eliminated in the first
step of the construction, differ.
be an annotated revision program and let B I
and BR be T 2 -valuations. The F-reduct of P with respect to (B I ; BR ) (denoted
BR jB I ) is defined as follows:
1. Remove from P every rule whose body contains an annotated revision atom
that is not satisfied in BR .
2. From the body of each remaining rule delete any annotated revision atom
that is satisfied in B I .
The notion of justified revision as defined by Fitting differs from our notion
only in that the necessary change of the F-reduct is used. We call the justified
revision using the notion of F -reduct, the F-justified revision.
In the remainder of this section we show that the notion of the F-justified
revision does not in general satisfy some basic requirements that we would like
justified revisions to have. In particular, F-justified revisions under an annotated
revision program P are not always models of P .
Example 1. Consider the lattice T fp;qg . Let P be a program consisting of the
following rules:
(in(a):fpg) / (in(b):fp; qg) and (in(b):fqg) /
and let B I be an initial valuation such that B I (a) = h;; ;i and B I (b) = hfpg; ;i.
Let BR be a valuation given by BR
is an F -justified revision of B I (under P ). However, BR
does not satisfy P .
The semantics of F -justified revisions also fails to satisfy the invariance under
join property.
Example 2. Let P be a revision program consisting of the following rules:
(in(a):fpg) / (in(b):fp; qg) and (in(b):fqg) /
and let P 0 consist of
(in(a):fpg) / (in(b):fpg); (in(b):fqg) and (in(b):fqg) /
Let the initial valuation B I be given by B I (a) = h;; ;i and B I (b) = hfpg; ;i. The
only F-justified revision of B I (under P ) is a T 2 -valuation BR , where BR
h;; ;i and BR ;i. The only F-justified revision of B I (under
is a T 2 -valuation B 0
replacing in the body of a rule annotated revision atom (in(b):fp; qg) by (in(b):
fpg) and (in(b):fqg) affects F-justified revisions.
However, in some cases the two definitions of justified revision coincide. The
following result provides a complete characterization of those cases.
Theorem 4. F-justified revisions and justified revisions coincide if and only if
the lattice T is linear (that is, for any two elements
Theorem 4 explains why the difference between the justified revisions and F -
justified revisions is not seen when we limit our attention to revision programs
as those considered in [MT98]. Namely, the lattice T of boolean
values is linear. Similarly, the lattice of reals from the segment [0; 1] is linear,
and there the differences cannot be seen either.
5 Properties of justified revisions
In this section we study basic properties of justified revisions. We show that
key properties of justified revisions in the case of revision programs without
annotations have their counterparts in the case of justified revisions of annotated
revision programs.
First, we will observe that revision programs as defined in [MT95] can be
encoded as annotated revision programs (with annotations taken from the lattice
Namely, a revision rule
(where p and all q i s are revision atoms) can be encoded as
In [Fit95], Fitting argued that under this encoding the semantics of F-justified
revisions generalizes the semantics of justified revisions introduced in [MT95].
Since for lattices whose ordering is linear the approach by Fitting and the approach
presented in this paper coincide, and since the ordering of T WO is linear,
the semantics of justified revisions discussed here extends the semantics of justified
revisions from [MT95].
Next, let us recall that in the case of revision programs without annotations,
justified revisions under a revision program P are models of P . In the case of
annotated revision programs we have a similar result.
Theorem 5. Let P be an annotated revision program and let B I and BR be
-valuations. If BR is a P -justified revision of B I then BR is a c-model of P
(and, hence, also a model of P ).
In the case of revision programs without annotations, a model of a program
P is its unique P -justified revision. In the case of programs with annotations,
the situation is slightly more complicated. The next result characterizes those
models of an annotated revision program that are their own justified revisions.
Theorem 6. Let a T 2 -valuation B I be a model of an annotated revision program
I is a P -justified revision of itself if and only if B I is a c-model of
As we observed above, in the case of programs without annotations, models
of a revision program are their own unique justified revisions. This property does
not hold, in general, in the case of annotated revision programs.
Example 3. Consider an annotated revision program P (with annotations belonging
to T fp;qg ) consisting of the clauses:
(out(a):fqg) / and (in(a):fqg) / (in(a):fqg)
Consider a T 2 -valuation B I such that B I (a) = hfqg; fqgi. It is easy to see that
B I is a c-model of P . Hence, B I is its own justified revision (under P ).
However, B I is not the only P -justified revision of B I . Consider the T 2 -
valuation BR such that BR (a) = h;; fqgi. We have PBR jB I = f(out(a):fqg) /g.
Let us denote the corresponding necessary change, NC(PBR jB I ), by C. Then,
BR (a). Consequently, BR is a P -justified revision of B I .
The same behavior can be observed in the case of programs annotated with
elements from other lattices.
Example 4. Let P be an annotated revision program (annotations belong to the
lattice consisting of the rules:
I be a valuation such that B I (a) = h0:4; 1i. Then, B I is a c-model of
and, hence, it is its own P -justified revision. Consider a valuation BR such
that BR (a) = h0; 1i. We have PBR jB I us denote the
necessary change NC(PBR jB I ) by C. Then
Thus, ((B
(a). That is, BR is a P -justified revision
of B I .
Note that in both examples the additional justified revision BR of B I is
smaller than B I with respect to the ordering - k . It is not coincidental as demonstrated
by our next result.
Theorem 7. Let B I be a model of an annotated revision program P . Let BR be
a P -justified revision of B I . Then, BR - k B I .
Finally, we observe that if a consistent T 2 -valuation is a model (or a c-model;
these notions coincide in the class of consistent valuations) of a program then,
it is its unique justified revision.
Theorem 8. Let B I be a consistent model of an annotated revision program P .
I is the only P -justified revision of itself.
To summarize, when we consider inconsistent valuations (they appear natu-
rally, especially when we measure beliefs of groups of independent experts), we
encounter an interesting phenomenon. An inconsistent valuation B I , even when
it is a model of a program, may have different justified revisions. However, all
these additional revisions must be less informative than B I . In the case of consistent
models this phenomenon does not occur. If a valuation B is consistent
and satisfies P then it is its unique P -justified revision.
6 An alternative way of describing annotated revision
programs and order-isomorphism theorem
We will now provide an alternative description of annotated revision programs.
Instead of evaluating separately revision atoms (i.e. expressions of the form in(a)
and out(a)) we will evaluate atoms. However, instead of evaluating revision
atoms in T , we will evaluate atoms in T 2 (i.e. T \Theta T ). This alternative presentation
will allow us to obtain a result on the preservation of justified revisions
under order isomorphisms of T 2 . This result is a generalization of the "shift
theorem" of [MPT99].
An expression of the form ahff; fii, where hff; fii 2 T 2 , will be called an annotated
atom (thus, annotated atoms are not annotated revision atoms). Intuitively,
an atom ahff; fii stands for both (in(a):ff) and (out(a):fi). An annotated rule
is an expression of the form p / q are annotated
atoms. An annotated program is a set of annotated rules.
satisfies an annotated atom ahff; fii if hff; fii - k B(a).
This notion of satisfaction can be extended to annotated rules and annotated
programs.
We will now define the notions of reduct, necessary change and justified
revision for the new kind of program. The reduct of a program P with respect
to two valuations B I and BR is defined in a manner similar to Definition 2.
Specifically, we leave only the rules with bodies that are satisfied by BR , and
in the remaining rules we reduce the annotated atoms (except that now the
transformation ' is no longer needed!). Next, we compute the least fixpoint of
the operator associated with the reduced program. Finally, as in Definition 3,
we define the concept of justified revision of a valuation B I with respect to a
revision program P .
It turns out that this new syntax does not lead to a new notion of justified
revision. Since we talk about two different syntaxes, we will use the term "old
syntax" to denote the revision programs as defined in Section 2, and "new syn-
tax" to describe programs introduced in this section. Specifically we now exhibit
two mappings. The first of them, tr 1 , assigns to each "old" in-rule
(in(a):ff)
a "new" rule
Encoding of an "old" out-rule
is analogous:
Translation tr 2 , in the other direction, replaces a revision "new" rule by one
in-rule and one out-rule. Specifically, a "new" rule
an hff
is replaced by two "old" rules (with identical bodies but different heads)
(in(a):ff)
and
The translations tr 1 and tr 2 can be extended to programs. We then have the
following theorem.
Theorem 9. Both transformations tr 1 , and tr 2 preserve justified revisions. That
are valuations in T 2 and P is a program in the "old" syntax, then
BR is a P -justified revision of B I if and only if BR is a tr 1 (P )-justified revision
of B I . Similarly, if B I ; BR are valuations in T 2 and P is a program in the
"new" syntax, then BR is a P -justified revision of B I if and only if BR is a
tr 2 (P )-justified revision of B I .
In the case of unannotated revision programs, the shifting theorem proved in
[MPT99] shows that for every revision program P and every two initial databases
there is a revision program P 0 such that there is a one-to-one correspondence
between P -justified revisions of B and P 0 -justified revisions of B 0 . In
particular, it follows that the study of justified revisions (for unannotated pro-
grams) can be reduced to the study of justified revisions of empty databases. We
will now present a counterpart of this result for annotated revision programs.
The situation here is more complex. It is no longer true that a T 2 -valuation can
be "shifted" to any other T 2 -valuation. However, the shift is possible if the two
valuations are related to each other by an order isomorphism of the lattice of all
There are many examples of order isomorphisms on the lattice of T 2 -valua-
tions. For instance, the mapping defined by /(hff;
is an order isomorphism of T 2 . In the case of a specific lattice
isomorphisms of T 2
are generated by permutations of the set X . An order isomorphism
on T 2 can be extended to annotated atoms, programs and valuations.
The extension to valuations is again an order isomorphism, this time on the
lattice of all T 2 -valuations.
The following result generalizes the shifting theorem of [MPT99].
Theorem 10. Let / be an order-isomorphism on the set of T 2 -valuations. Then,
BR is a P -justified revision of B I if and only if /(BR ) is a /(P )-justified revision
of /(B I ).
7 Conclusions and further research
The main contribution of our paper is a new definition of the reduct (and hence of
justified revision) for the annotated programs considered by Fitting in [Fit95].
This new definition eliminates some anomalies (specifically the fact that the
justified revisions of [Fit95] do not have to be models of the program). We also
found that in cases where the intuition of [Fit95] is very clear (for instance in case
when annotations are numerical degrees of belief), the two concepts coincide.
Due to the limited space of the extended abstract, some results were not
included. Below we briefly mention two research areas that are not discussed
here but that will be discussed in the full version of the paper.
First, the annotation programs can be generalized to disjunctive case, that
is to programs admitting "nonstandard disjunctions" in the heads of rules. It
turns out that a definition of justified revisions by means of such programs is
possible, and one can prove that the disjunctive revisions for programs that have
the head consisting of just one literal reduce to the formalism described above.
Second, one can extend the formalism of annotated revision programs to the
case when the lattice of annotations is not distributive. However, in such case
only some of the results discussed here still hold.

Acknowledgments

This work was partially supported by the NSF grants CDA-9502645 and IRI-
9619233.



--R


Annotated revision specification programs.
Fixpoint semantics for logic programming - a survey
Multivalued logics: a uniform approach to reasoning in artificial intelligence.
Theory of generalized annotated logic programs and its applications.
Answer sets in general nonmonotonic reasoning.
Revision programming
Revision programming
Revision programming.
Update by means of inference rules.
The Mathematics of metamathematics.
--TR
Quantitative deduction and its fixpoint theory
Theory of generalized annotated logic programming and its applications
Stable semantics for probabilistic deductive databases
Revision programming
The Semantics of Predicate Logic as a Programming Language
Fixpoint semantics for logic programming a survey
Revision Programming, Database Updates and Integrity Constraints
Annotated Revision Specification Programs
Revision Programming = Logic Programming

--CTR
Logic programming and knowledge representation-the A-prolog perspective, Artificial Intelligence, v.138 n.1-2, p.3-38, June 2002
database updates;annotated programs;belief revision;revision programming;knowledge representation