=Paper= {{Paper |id=Vol-2445/paper_2 |storemode=property |title=WHIWAP: Checking Iterative Belief Changes |pdfUrl=https://ceur-ws.org/Vol-2445/paper_2.pdf |volume=Vol-2445 |authors=Kai Sauerwald,Jonas Haldimann |dblpUrl=https://dblp.org/rec/conf/ki/SauerwaldH19 }} ==WHIWAP: Checking Iterative Belief Changes== https://ceur-ws.org/Vol-2445/paper_2.pdf

Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

Whiwap: Checking Iterative Belief Changes

Kai Sauerwald and Jonas P. Haldimann

FernUniversität in Hagen, 58084 Hagen, Germany
{kai.sauerwald,jonas.haldimann}@fernuni-hagen.de

Abstract. In the framework for iterative belief revision by Darwiche
and Pearl, epistemic states are equipped with a total preorder on possible
worlds. Belief changes in this framework not only aﬀect the set of formulas
that are considered to be true but the whole preorder. Diﬀerent postulates
were proposed to confine the changes of total preorders. We present
Whiwap, a tool which allows the user to enter a belief change with a
propositional formula ↵, in particular to specify the total preorder of the
prior and the posterior state and the models of ↵. Whiwap checks whether
the entered belief change fulfils certain postulates or not. Common belief
change postulates for revision and contraction are implemented.

Keywords: belief change, postulate, total preorder, epistemic state

1 Introduction
In the well established framework for iterative belief revision by Darwiche and
Pearl [6], epistemic states are equipped with a total preorder on possible worlds.
Belief change in this framework not only aﬀects the set of formulas that are
considered to be true, but the whole preorder. The motivation for using these
more complex structure is the insight by Darwiche and Pearl, that using belief
sets is not expressive enough for the task of iterative belief change. Moreover,
total preorders are the right semantics for iterative change in the light of very
fundamental principles of change, which respect conditional beliefs.
Belief revisions, belief contractions and other kinds of belief changes in the
framework of total preorders are still a subject of interest, and so far a lot of
diﬀerent postulates have been proposed to confine the changes on total preorders.
And sometimes you want to check if a certain belief change fulfils some postulate
or not. Researchers in the field are often searching for counterexamples - or
are just curious about the properties of some belief change operator. To avoid
doing such checks manually, which is not only tedious but also error-prone, we
developed Whiwap (short for "What sHoud I do With All these Postulates?").
Typically, iterative belief change operators are defined syntactically and then
a representation theorem connects the syntactical definition with a semantic
equivalent, where the semantics is commonly a total preorder semantics. Whiwap
works mainly on the semantic side, it allows to enter a total preorder before and
after a change with a certain formula and analyses what postulates are fulfilled by
this change. Whiwap has implemented checks for common revision postulates as
well as contraction postulates, and the set of postulates is extended continuously.

14
In this paper we present Whiwap as follows: In Section 2 the basics on belief
change in the Darwiche and Pearl-framework of total preorders are presented.
After that Whiwap is described in more detail in Section 3. Finally we give a
discussion and an outlook to future work in Section 4.

2 Preliminaries and Background
Let ⌃ be a propositional signature and L be the propositional language over
⌃. We denote formulas in L with lower Greek letters ↵, , , . . ., and proposi-
tional variables with lower case letters a, b, c, . . . 2 ⌃. The set of propositional
interpretations ⌦, also called set of worlds, is identified with the set of corre-
sponding complete conjunctions over ⌃. Propositional entailment is denoted by
|=, with J↵K we denote the set of models of ↵, and Cn(↵) = { | ↵ |= } is the
deductive closure of ↵. A total preorder  over ⌦ is a relation which fulfils for
all !, !1 , !2 , !3 2 ⌦:

(reflexivity) !!
(transitivity) !1  !2 and !2  !3 implies !1  !3
(totality) !1  !2 or !2  !1

For a total preorder , we denote with < its strict variant, i.e. x < y iﬀ x  y
and y 6 x; and we write x ' y iﬀ x  y and y  x. For a set of worlds
⌦ 0 ✓ ⌦ and a total preorder  over ⌦, we denote with min(⌦ 0 , ) = {! | ! 2
⌦ 0 and there is no ! 0 2 ⌦ 0 s.t. ! 0 < !} the set of all worlds in the lowest layer
of  that are elements in ⌦ 0 .

2.1 Belief Change in the Darwiche-Pearl Framework
The research in the Darwiche-Pearl framework (DP-framework) of belief change
focusses on mainly two kinds of belief changes: incorporating new information
into the beliefs of an agent (revision) and removing a belief from an agent’s beliefs
(contraction). This is inherited from the AGM-Theory (named after Alchourrón,
Gärdenfors and Makinson [1]), which deals with the change of theories, instead
of epistemic states.
Technically, in the DP-framework beliefs are propositional formulas from
L. The beliefs of an agent are represented indirectly by a total preorder  of
possible worlds, where denotes the epistemic state of an agent. Here, possible
worlds are identified with propositional interpretations !, !1 , !2 , . . . 2 ⌦. The
basic idea is, that the total preorder  represents the plausibility of the diﬀerent
worlds in ⌦, where !1  !2 means that the world !1 is more or equally plausible
than the world !2 . Consequently, the minimal elements of  are interpreted as
the most plausible worlds, denoted by k k = min(⌦,  ). The beliefs Bel ( )
of an agent with epistemic state are the set of beliefs that are compatible
with the most plausible worlds of  , i.e. define Bel ( ) = {↵ 2 L | for all ! 2
k k we have ! |= ↵}. This framework is very foundational, since many more

15
meticulous representation formalisms, like ranking functions [16], induce an total
preorder.
A belief change operator transforms an epistemic state and a formula
↵ into a new epistemic state ↵. Diﬀerent kind of changes, like revision and
contraction, are characterised in the DP-framework by axiomatic properties.
Semantically, the task of the operator is reduced to the question of how the
worlds should be shifted in the total preorder  to obtain  ↵ such that the
change obeys the axiomatic description of the changes. In the rest of this paper
we restrict ourselves only to the semantic side of (iterative) belief revision and
contraction, which is used by Whiwap.
Darwiche and Pearl showed that AGM revision [1], denoted here by ⇤, can be
reduced to one axiom in the DP-framework.

Proposition 1 (AGM Revision for Epistemic State [6]). A belief change
operator ⇤ is an AGM revision on epistemic states if and only if ⇤ satisfies:

(AGMes⇤ ) k ⇤ ↵k = min(J↵K,  )

Proposition 1 characterises AGM revision in the DP-framework as the operation
which makes the most plausible worlds of ↵ ultimately plausible.
More recently, a similar characterisation of contraction has been worked
out [5, 10]. Contraction of ↵ is the process of making the minimal counter worlds
of ↵ maximally plausible, while retaining the plausibility of non-counter worlds.

Proposition 2 (AGM Contraction for Epistemic State [10]). A belief
change operator ÷ is an AGM contraction on epistemic states if and only if ÷
satisfies:

(AGMes÷
) k ÷ ↵k = k k [ min(J¬↵K,  )

Observe that neither (AGMes⇤ ) nor (AGMes÷  ) constrain how worlds in
layers above the minimal layer of  should be ordered. Darwiche and Pearl
showed that this is problematic, as it lead to counter-intuitive changes [6]. In
the following, we present postulates for diﬀerent solutions to the problem of how
changes of the non-minimal layers should be constrained.

2.2 General Postulates for Iteration

Proposition 1 and Proposition 2 define revision and contraction in the DP-
framework. However, iterative belief change also requires to handle maintenance
information for the change strategy of , which is encoded in the total preorder
 . Neither the postulate (AGMes⇤ ) nor (AGMes÷  ) give much insight on how
to maintain the strategy informations.
Darwiche and Pearl [6] propose that the order of plausible worlds should
be retained under reasonable circumstances. This is a natural extension of the

16
principle of minimal change from the original AGM approach [1].

(DP1) if !1 , !2 2 J↵K, then !1  !2 , !1  ⇤↵ !2
(DP2) if !1 , !2 2 J¬↵K, then !1  !2 , !1  ⇤↵ !2
(DP3) if !1 2 J↵K and !2 2 J¬↵K, then !1 < !2 ) !1 < ⇤↵ !2
(DP4) if !1 2 J↵K and !2 2 J¬↵K, then !1  !2 ) !1  ⇤↵ !2

A revision with ↵ separates the possible worlds in two kinds: the ones that model
↵ and the ones that do not model ↵. The postulates (DP1) and (DP2) guarantee
that worlds of each kind keep their order. Moreover, (DP3) and (DP4) guarantee
that models of ↵ stay more plausible then counter-models if they were more
plausible before.
For contraction a similar set of postulates has been proposed [5, 10]:

(IC1) if !1 , !2 2 J↵K, then !1  !2 , !1  ÷↵ !2
(IC2) if !1 , !2 2 J¬↵K, then !1  !2 , !1  ÷↵ !2
(IC3) if !1 2 J¬↵K and !2 2 J↵K, then !1 < !2 ) !1 < ÷↵ !2
(IC4) if !1 2 J¬↵K and !2 2 J↵K, then !1  !2 ) !1  ÷↵ !2

The postulates (IC1) and (IC2) implement the same idea as (DP1) and (DP2).
Analogue to (DP3) and (DP4) the postulates (IC3) and (IC4) state that a
contraction which obeys this properties should never disimprove the relative
plausibility of counter-models.

2.3 Strategies for Iterative Belief Change
Another approach to iterated change is the implementation of concrete change
strategies. Many concrete strategies have semantic representations in the DP-
framework. The class of operators implementing a specific strategy for revision
(respectively contraction) are characterised in the DP-framework by demanding
additional postulates in addition to the success postulate (AGMes⇤ ) (respectively
(AGMes÷  ))

Natural Change One of the most well-known strategy for revision is introduced by
Boutiller [4], often called natural revision. The approach of natural change is to
retain as much as possible of the conditional beliefs. An equivalent of this strategy
for revision is translated into the DP-framework by Darwiche and Pearl [6]:

(CBR) if !1 , !2 2
/ k ⇤ ↵k, then !1  !2 , !1  ⇤↵ !2

Operators which obey the postulate (CBR) keep as much of the old ordering as
possible. Ramachandran, Nayak and Orgun [13] formulate natural contraction
similar to (CBR) as follows:

(NC1) if !1 2 k k or !1 2 min(J¬↵K,  ), then !1  ÷↵ !2
(NC2) if !1 , !2 2
/ k k [ min(J¬↵K,  ), then !1  !2 , !1  ÷↵ !2

17
Lexicographic Change Another revision strategy introduced by Nayak, Pagnucco
and Peppas [12] is to order the worlds by whether they satisfy the information ↵
or not. This policy is given by the following postulate:

(SimpLex) if !1 2 J↵K and !2 2 J¬↵K, then !1 < ⇤↵ !2

Transferring the principle of lexicographic change to contraction has been pro-
posed, but is not as straightforward as for revision. Due to complexity of the
approach we refer the interested reader to the work of Ramachandra, Nayak and
Orgun [13].

Admissible and Restrained Revision The strategy of admissible revision with ↵
enforces improvement of worlds that comply with ↵. This has been proposed
under the name independence by Jin and Thielscher [9] and is characterised in
the light of (AGMes÷
 ) as follows:

(PR) if !1 2 J↵K and !2 2 J¬↵K, then !1  !2 ) !1 < ⇤↵ !2

The strategy of admissibility has been further supplemented by Booth and
Meyer [3] with the idea of overwriting the believability of counteracting beliefs
by a revision. It can be shown that this is equal to the following principle (DR):

(DR) if !1 2 J¬↵K, !2 2 J↵K and !2 2
/ k ⇤ ↵k, then !1 < !2 ) !1 < ⇤↵ !2

Moderate Contraction The idea of moderate contraction or also called priority
contraction [14], is that a removal of ↵ should also decrease the plausibility of at
least one of the implications ! ↵ or ¬ ! ↵. This is captured semantically in
the DP-framework by the following set of postulates by Ramachandra, Nayak,
Orgun [13] in the light of (IC1) and (IC2):

(MC3) if !1 2 J↵K, !1 2
/ k k,  ) and !2 |= ¬↵, then !2 < ÷↵ !1
(MC4) if !1 2 min(⌦,  ) or !1 2 min(J¬↵K,  ), then !1  ÷↵ !2

In the literature many more classes of operators and their representation
in the DP-framework can be found (e.g. [14]). In the following we present how
Whiwap can be used to check whether these postulates are satisfied or not.

3 Whiwap

Whiwap allows to check whether a certain revision fulfils a given set of belief
change postulates. In this section we will first describe the user interface of the
tool. Afterwards we will give a short overview of the implementation.

18
Fig. 1: User interface for setting the signature size. The set of all worlds with this
signature is shown on the right side.

..
.
P2 layer 2 āb̄
P1 layer 1 āb āb̄ layer 1 āb ab̄
P0 layer 0 ab ab̄ layer 0 ab
(a) Every layer contains (b) Example of a total pre- (c) Example of a total pre-
a partition. The lower a order. The worlds where order. The world ab is con-
layer, the more plausible. a is true are considered sidered to be plausible, the
to be plausible, the worlds worlds āb and ab̄ less plau-
where a is not true, not. sible and āb̄ least plausi-
ble.

Fig. 2: Representing total preorders with layers.

3.1 User Interface

To analyse a belief change, the tool requires the epistemic states before and after
the change as well as a change parameter. One of the main functions of the UI is
to allow the user to enter this information.
The user starts by entering the size of the signature with a slider. The tool
automatically selects the first characters of the alphabet as the signature ⌃ and
generates the set of all possible worlds ⌦ over ⌃ (see Figure 1).
As described in Section 2, an epistemic state can be represented by a total
preorder on all worlds in the DP-framework. Every total preorder induces an
ordered partition P0 [˙ . . . [P
˙ n = ⌦ of the worlds. Two worlds !1 , !2 are in the
same partition, if and only if !1  !2 and !2  !1 . If two worlds !1 2 Pi and
!2 2 Pj are in diﬀerent sets, it holds that !1  !2 and !2 ⇥ !1 if and only if
i < j. This partition in turn can be displayed with layers (see Figure 2). The
worlds in the set P0 , i.e. the minimal worlds with respect to the total preorder,
are placed in the lowest layer, the worlds in P1 in the second lowest layer and so
on. In particular we have P0 = k k.
The user interface uses this concept of layers to realise an intuitive input of
total preorders. Layers are indicated by lines, worlds by small boxes above the
line of the layer they are placed in. Initially, all worlds are placed in the lowest
layer, which corresponds to a total preorder where all worlds are considered
equally plausible. From there, worlds can be moved around via ‘drag and drop’.
If a world is placed in the highest displayed layer, the next layer is added to the

19
visualisation. Empty layers are removed automatically. A screenshot of this part
of the user interface is shown in Figure 3.
The parameter ↵ of a belief change is in fact a propositional formula over ⌃.
As we only consider the semantics of ↵, the user does not have to type in the
formula but only specifies the interpretations that satisfy ↵. For this, the user
interface displays a list of all interpretations. The interpretations can be selected
by clicking on them. Selected interpretations are highlighted by diﬀerent colours
(see Figure 3).
After the ‘Check belief change’-Button is clicked, the belief change is analysed
and the results are displayed in a table (see Figure 4), which shows which
postulates are fulfilled. If the mouse hovers over a postulates name, a tooltip
with a summary of the postulate is displayed. For the convenience of the user
the postulates are grouped.

Example Consider the situation where the initial epistemic state is associated
with the total preorder displayed in Figure 2b: The worlds ab and ab̄ are equally
plausible. The worlds āb and āb̄ are also equally plausible but both less plausible
than ab and ab̄. We will further assume that the change happens under the
proposition ↵ = b. The preorder of the resulting epistemic state is the one
displayed in Figure 2c: The world ab is considered most plausible. The worlds
where one of a or b is false are considered equally plausible and less plausible
than ab. The world āb̄ is even less plausible.
Figure 3 shows how this belief change looks in Whiwap. The total preorders
are visualized by their corresponding layers. The proposition b is entered by
selecting ab and āb which are the interpretations of b. The result table for this
change is displayed in Figure 4. The four Darwiche-Pearl postulates are fulfilled
by this change, because the worlds fulfilling b (which are ab and āb) do not change
their order among each other, and the worlds not fulfilling b̄ (which are ab̄ and
āb̄) do not change their order among each other. However, (DR) is not satisfied
by this change. For an counter-example consider !1 = ab and !2 = ab. Then we
have !1 < !2 and !2 2 /k ↵k, but !1 ' ↵ !2 .

Fig. 3: User interface to enter a belief change. The worlds in the epistemic states
can be moved via ‘drag and drop’. The worlds which satisfy ↵ can be selected by
clicking on them in the proposition UI.

20
...
Fig. 4: The result of the analysis is displayed in a table. This figure shows only
the first part of the table.

3.2 Some Technical Details

Whiwap consists of two parts: A frontend to provide the user interface and a
backend to check the postulates.
The frontend is a web application build with HTML, CSS and JavaScript.
It manages the user interactions and displays information. When the revision
postulates are to be checked, the frontend encodes the epistemic states and
parameters as JSON and sends them to the backend. As a response it receives
a list of postulates, their descriptions, and a table listing which postulates are
fulfilled for the revision. The frontend displays this data.
The backend is a small Java application running on a server. It receives the
requests from the frontend and replies with a list of postulates, their descriptions,
and a table listing which postulates are fulfilled for each revision step. The
check for each postulate is implemented in a straightforward way. E.g., consider
postulate DP1: Two nested loops iterate over all combinations (!1 , !2 ) of the
worlds that both satisfy ↵ and check if (!1 , !2 ) is in the preorder before the
change if and only if it is in the preorder after the change. The complexity of
testing whether a change fulfils a postulate is polynomial1 in the size of the total
preorders. However, a total preorder orders all interpretations, and thus, its size
is exponential in relation to the signature. We refer the interested reader to an
article by Liberatore on the general complexity of iterative change [11].

1
for most of the above mentioned postulates

21
4 Discussion and Future Work

In this paper we introduced Whiwap, a tool that allows to quickly check what
postulates are fulfilled by a certain change on epistemic states in the Darwiche-
Pearl framework. In Section 3 we described the user interface and gave an overview
over the technical realisation. Before we gave a presentation on the technical
background in Section 2. The tool Whiwap is available online at:

https://www.fernuni-hagen.de/wbs/alchourron/

To the best of our knowledge there is no tool like Whiwap, which builds on the
Darwiche-Pearl framework. However, there are some implementations for belief
change in the (classical) setting of belief sets [2, 7, 8].
We believe that total preoders used by the Darwiche-Pearl framework are an
intuitive base for belief change and reasoning. While this introduction given here
is very technical, there are many applications of the framework. For instance, it
might be interesting for psychology, where total preorders could act as mental
representation, and thus, help in the task of analysing and formalising belief
change of humans. Such a connection has been drawn [15].
For future work, we see many possibilities of advancing Whiwap. So far,
Whiwap can only analyse one change at a time. A later version should allow the
user to enter several change steps at once. The next step will be to improve the
user interface such that counter-examples are presented for postulates that are
not satisfied. Furthermore, it is our goal to advance Whiwap in such a way that
it will predict the result of a belief change given only two of the ingredients of
 , ↵ or  ↵ in the light of a selection of belief change postulates.

Acknowledgements

This work was supported by DFG Grant BE 1700/9-1 awarded to Christoph
Beierle as part of the priority program "Intentional Forgetting in Organizations"
(SPP 1921). Kai Sauerwald is supported by this Grant.

References

1. Alchourrón, C.E., Gärdenfors, P., Makinson, D.: On the logic of theory change:
Partial meet contraction and revision functions. J. Symb. Log. 50(2), 510–530
(1985)
2. Beierle, C., Kern-Isberner, G.: A verified AsmL implementation of belief revision.
In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Abstract State Machines, B
and Z. pp. 98–111. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)
3. Booth, R., Meyer, T.A.: Admissible and restrained revision. J. Artif. Intell. Res.
26, 127–151 (2006)
4. Boutilier, C.: Iterated revision and minimal change of conditional beliefs. J. Philo-
sophical Logic 25(3), 263–305 (1996)

22
5. Chopra, S., Ghose, A., Meyer, T.A., Wong, K.: Iterated belief change
and the recovery axiom. J. Philosophical Logic 37(5), 501–520 (2008).
https://doi.org/10.1007/s10992-008-9086-2
6. Darwiche, A., Pearl, J.: On the logic of iterated belief revision. Artificial Intelligence
89, 1–29 (1997)
7. Dixon, S., Wobcke, W.: The implementation of a first-order logic AGM belief revision
system. In: Fifth International Conference on Tools with Artificial Intelligence,
ICTAI ’93, Boston, Massachusetts, USA, November 8-11, 1993. pp. 40–47. IEEE
Computer Society (1993). https://doi.org/10.1109/TAI.1993.633934
8. Hunter, A., Tsang, E.: Genb: A general solver for AGM revision. In: Michael, L.,
Kakas, A.C. (eds.) Logics in Artificial Intelligence - 15th European Conference,
JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings. Lecture Notes
in Computer Science, vol. 10021, pp. 564–569 (2016). https://doi.org/10.1007/978-
3-319-48758-8_40
9. Jin, Y., Thielscher, M.: Iterated belief revision, revised. Artif. Intell. 171(1), 1–18
(2007)
10. Konieczny, S., Pino Pérez, R.: On iterated contraction: syntactic characterization,
representation theorem and limitations of the Levi identity. In: Scalable Uncertainty
Management - 11th International Conference, SUM 2017, Granada, Spain, October
4-6, 2017, Proceedings. Lecture Notes in Artificial Intelligence, vol. 10564. Springer
(2017)
11. Liberatore, P.: The complexity of iterated belief revision. In: Afrati, F.N., Kolaitis,
P.G. (eds.) Database Theory - ICDT ’97, 6th International Conference, Delphi,
Greece, January 8-10, 1997, Proceedings. Lecture Notes in Computer Science,
vol. 1186, pp. 276–290. Springer (1997)
12. Nayak, A.C., Pagnucco, M., Peppas, P.: Dynamic belief revision operators. Artif.
Intell. 146(2), 193–228 (2003)
13. Ramachandran, R., Nayak, A.C., Orgun, M.A.: Three approaches to iterated belief
contraction. J. Philosophical Logic 41(1), 115–142 (2012)
14. Rott, H.: Shifting Priorities: Simple Representations for Twenty-Seven Iterated
Theory Change Operators, pp. 269–296. Springer Netherlands, Dordrecht (2009).
https://doi.org/10.1007/978-1-4020-9084-4_14
15. Sauerwald, K.: Student research abstract: Modelling the dynamics of forgetting
and remembering by a system of belief changes. In: The 34th ACM/SIGAPP
Symposium on Applied Computing (SAC ’19), April 8–12, 2019, Limassol, Cyprus.
ACM, New York, NY, USA (2019). https://doi.org/10.1145/3297280.3297391
16. Spohn, W.: Ordinal Conditional Functions: A Dynamic Theory of Epistemic States,
pp. 105–134. Springer Netherlands, Dordrecht (1988)