=Paper=
{{Paper
|id=Vol-2961/paper_3
|storemode=property
|title=On Using Model Checking for the Certification of Iterated Belief Changes
|pdfUrl=https://ceur-ws.org/Vol-2961/paper_3.pdf
|volume=Vol-2961
|authors=Kai Sauerwald,Philip Heltweg
|dblpUrl=https://dblp.org/rec/conf/ki/SauerwaldH21
}}
==On Using Model Checking for the Certification of Iterated Belief Changes==
https://ceur-ws.org/Vol-2961/paper_3.pdf
Proceedings of the 7th Workshop on Formal and Cognitive Reasoning
On Using Model Checking for the Certification
of Iterated Belief Changes
Kai Sauerwald[0000 0002 1551 7016] and Philip Heltweg
FernUniversität in Hagen, 58084 Hagen, Germany
Abstract. The theory of iterated belief change investigates how epistemic
states are changed according to new beliefs. This is typically done by
focussing on postulates that govern how epistemic states are changed. A
common realisation of epistemic states are total preorders over possible
worlds. In this paper, we consider the problem of certifying whether an
operator over total preorders satisfies a given postulate. We introduce
the first-order fragment FOTPC for expressing belief change postulates
and present a way to encode information on changes into an FOTPC -
structure. As a result, the question of whether a belief change fulfils a
postulate becomes a model checking problem. We developed Alchourron,
an implementation of our approach, consisting of an extensive Java library,
and also of a web interface, which suits didactic purposes and experimental
studies. For Alchourron, we also present an evaluation of the running
time with respect to logical properties.
Keywords: Belief Change · Total Preorder · Implementation.
1 Introduction
A fundamental problem for intelligent agents is adapting their world-view to
potentially new and conflicting information. Iterated belief change discusses
properties of operators that model transition of currently held beliefs under newly
received information. The field has a large body of literature with di↵erentiated
results for a large variety of di↵erent types of operations, e.g., revision [6,5],
contraction [8,12,19], expansion, the area of non-prioritized change [11,3,22] and
many more [21].
The research on (iterated) belief change is focussed on propositional logic (but
not limited to). Often, total preorders over interpretations [6,11,3,21,19,22,12,22]
or refinements thereof [8,5] are considered as a representation formalism for
epistemic states.
A common aspect of many approaches in the area of iterated belief change is
that a class of operators is given by syntactic postulates, constraining how to
change, and that representation theorems show, which semantic postulates exactly
reconstruct that class of operators in the realm of total preorders. The typical
structure of postulates, regardless of whether they are syntactic or semantic
postulates; is that they focus on a single (but arbitrary) epistemic state and
constrain the result of subsequent changes on that state. When total preorders
Copyright c 2021 for this paper by its authors. Use permitted under
Creative Commons License Attribution 4.0 International (CC BY 4.0).
23
On Using Model Checking for the Certification of Iterated Belief Changes
are considered as epistemic states, then very often, the so-called faithfulness
condition and a representation theorem connects the syntactic viewpoint with
the semantic perspective, e.g. [6].
Given the large variety of di↵erent postulates and types of operations, it
is tedious and cumbersome to check manually whether a given specific change
satisfies a certain postulate, or to decide whether the change falls into a certain
category of type of operation.
This leads to the general problem of checking whether a belief change operator
or a singular change satisfies a given syntactic or semantic postulate, which we
call the certification problem. The certification problem got not much atten-
tion, notable exceptions are results about the complexity for specific operations
[16,13,20] and results about inexpressibility [25]. Furthermore, there seems to be
no implementation for the certification problem for the area of iterated belief
change.
In this paper, we propose an approach to grasp the certification problem
for the case where total preorders are used as epistemic states and provide
an implementation. The approach consists of defining the first-order fragment
FOTPC , which is meant as a language for semantic postulates. To focus on
semantic postulates seems to be only a minor restriction, as, given the many
representation theorems, many syntactic postulates are known to be expressible
by semantic postulates in the total preorder realm. Second, we describe how
an FOTPC -structure can be constructed for a belief change operator or for a
singular belief change. The certification problem then becomes a first-order model-
checking problem. Third, we provide an implementation of the approach, which
is publicly available on the web. We present an evaluation of the di↵erent steps
of the approach according to the computation time with respect to the signature
size and quantifier rank of postulates.
This paper extends recent work [18] by an empirical evaluation.
2 Belief Change on Epistemic States
Let L be a propositional language over a finite signature of propositional variables
⌃, and ⌦ its corresponding set of interpretations. Following the framework of
Darwiche and Pearl [6], we deal with belief changes over epistemic states and
propositions. An epistemic state is an abstract entity from a set E, where each
2 E is equipped with a deductively closed set Bel( ). A belief change operator
is a function : E ⇥ L ! E. In this paper, we only consider operators satisfying
the following syntax-independence condition for each 2 E and ↵, 2 L:
(sAGM5es*) if ↵ ⌘ , then ↵=
Here (sAGM5es*) is a stronger version of the extensionality postulate from the
revision approach by Alchourrón, Gärdenfors and Makinson [1] (AGM).
The framework by Darwiche and Pearl is di↵erent from the classical setup for
belief revision theory by AGM [1], where deductively closed sets (called belief
sets) are used as states [7]. However, the richer structure of epistemic states is
24
On Using Model Checking for the Certification of Iterated Belief Changes
necessary to include the information required to capture the change strategy of
iterative belief change [6].
There are many possible instantiations of E; however, we will stick here to the
popular one by total preorders. More precisely, we consider total preorders over
⌦ that fulfil the so-called faithfulness condition [10,6], stating that the minimal
elements of each total preorder = 2 E are exactly the models of Bel( ), i.e.,
Mod(Bel( )) = min(⌦, ). Thus, in the scope of this paper, each total preorder
2 E is assumed to describe an epistemic state entirely.
3 Problem Statement
Postulates are central objects in the area of (iterative) belief change and are
grouped together to define classes of belief change operators in a descriptive way.
The problem we address is to check whether a given operator satisfies a postulate,
i.e., belongs to a class of change operators specified by postulates. We call this
particular problem the certification problem (which could be considered as a
generalisation of the revision problem [16]):
Certification-Problem
Given: A belief change operator and a postulate P
Question: Does satisfy the postulate P ?
Clearly, information about a whole belief change operator is available or even
finitely representable only in few application scenarios. This gives rise to several
sub-problems depending on how much information of the particular operator
is known. Apart from the full operator , we consider the certification of the
following cases:
– A singular belief change from to 0 by ↵, i.e.: Does ↵ = 0 hold?
– A sequence of belief changes 1 ↵1 = 2 , and 2 ↵2 = 3 , and . . .
– All singular belief changes on a state , i.e. the set {( 1 , ↵, 2 ) 2 | = 1}
In the next section we present a model-checking based formalisation of the
Certification-Problem.
4 The Approach
In belief change, postulates are usually described by common mathematical
language, which is close to (first-order) predicate logic. In the following, we use
the toolset of first-order logic to formalise the Certification-Problem as a
first-order model-checking problem.
Language for Postulates. As an initial study, we considered several postulates
from the literature on iterated belief change, e.g. [6,4,9,2,15], and selected the
most common predicates and functions used. We compiled them into a fragment of
first-order logic with equality over a fixed set of predicates and function symbols1 ,
1
Note that we could also use a fragment of many-sorted first-order logic. However,
some predicates are ”overloaded” in respect to sorts.
25
On Using Model Checking for the Certification of Iterated Belief Changes
Predicate Intended meaning Exemplary appearance
M od(w, x) w is a model of x ! 2 Mod( ), ! 2 Mod(↵)
LessEQ(w1 , w2 , e) w1 w2 in e ! 1 !2
Int(w) w is an interpretation !2⌦
ES(e) e is an epistemic state 2E
F orm(a) a is a formula ↵2L
Function Intended meaning Exemplary appearance
op(e0 , a) op(e0 , a) is a result of changing e0 by a ↵= 0
or(a, b) propositional disjunction Bel( (↵ _ )) = . . .
not(a) propositional negation ¬↵ 2
/ Bel( ↵)
Fig. 1: Allowed predicates and functions symbols in FOTPC , their intended meaning
and how they are typically formulated in belief change literature.
denoted by FOTPC (Total Preorder Change), with the intention to describe
changes over total preorders. Figure 1 summarises the permitted symbols and
describes only the minimal required set.
Several common predicates and functions used in postulates are expressible
by the means of FOTPC by employing this minimal set, e.g. logical entailment,
semantic equality, the strict part of a total preorder, checking whether a formula
has no model, etc. For a specific example, consider the following:
LogImpl(x, y):=8w.Int(w)! (M od(w, x)!M od(w, y))
where LogImpl(x, y) describes that x logically implies y.
For illustration, we consider some aspects about belief change postulates.
First, belief change postulates are typically formulated with a locality aspect;
every postulate focusses on an initial state and a change formula ↵, describing a
condition for this change. As prominent examples, the following postulates are
an excerpt of the AGM revision postulates [1]:
(AGM2*) ↵ 2 Bel( ↵)
(AGM7*) Bel( (↵ ^ )) ✓ Cn(Bel( ↵)[{ })
TPC
In FO , we address this by reserving e0 and a as special terms, where e0 denotes
the initial state and a denotes the formula representing the new information.
Postulates for (iterated) belief change typically come in two fashions: Semantic
postulates describe changes in a semantic domain, such as faithful total preorders.
For example, consider the following postulate:
(CR1) if !1 , !2 2 Mod(↵), then !1 !2 , !1 ↵ !2
This could be expressed in FOTPC by the following formula 'CR1 :
'CR1 = 8w1 , w2 . (Int(w1 ) ^ Int(w2 ) ^ M od(w1 , a) ^ M od(w2 , a))
! (LessEQ(w1 , w2 , e0 ) $ LessEQ(w1 , w2 , op(e0 , a)))
26
On Using Model Checking for the Certification of Iterated Belief Changes
Universe U AC = ⌦ [ { 0 , 1 } [ P(⌦)
Predicates
M odAC = {(!, x) | x 2 P(⌦) [ { 0 , 1 }, ! 2 Mod(x)}}
IntAC = ⌦
ES AC = { 0 , 1 }
F ormAC = P(⌦)
LessEQAC = {(!1 , !2 , i ) | !1 i !2 }
Functions
orAC = ↵1 , ↵2 . ↵1 [ ↵2 eA
0
C
= 0
notAC = ↵1 . ⌦ \ ↵1 aAC = Mod(↵)
opAC = ({( , , ) | 2 P(⌦), 2 { 0 , 1 }} \ {( 0 , ↵, 0 }) [ {( 0 , ↵, 1 )}
Fig. 2: Structure AC , encoding a singular change C = ( 0 , ↵, 1)
On the other hand, syntactic postulates describe changes of Bel( ). Aside
of the AGM revision postulates, prominent examples are the Darwiche-Pearl
postulates for revision [6] such as:
(DP1) if |= ↵, then Bel( ↵ ) = Bel( )
Several representation results in the literature show how syntactic and semantic
postulates are interrelated. For instance, it is well-known that, given is an
AGM revision operator, (CR1) holds if and only if (DP1) holds [6]. Moreover,
the semantic and syntactic domains are of course related, which allows us to
describe many predicates used in the syntactic realm by semantic means. For
example, a statement like Bel( ↵ ) = Bel( ) is expressible in FOTPC by
employing the following formula:
Bel(a, e) := (F orm(a) ^ ES(e)) ! (8x.M od(x, a) $ M od(x, e))
We describe now how objects like belief change operators, singular changes
and so on are related to FOTPC formulas.
Encoding as Model-Checking. Internally, we use the standard truth-functional
semantics of first-order logic for FOTPC . Therefore, we translate a belief change
operator, or the known part of it, into a first-order structure.
The general idea is to define a structure A by the following pattern: The
universe U A consists of all propositional interpretations ⌦, all formulas from L
and all considered epistemic states from , i.e., the total preorders over ⌦. We
represent formulas by their models, i.e., by elements of2 P(⌦). The rationale
is that, because of (sAGM5es*), the considered belief change operators are in-
sensitive to syntactic variations. Additionally, predicates are interpreted in the
straight-forward manner, e.g., the predicate Int is interpreted as all propositional
interpretations, IntA = ⌦, and LessEQ allows access to the total preorder
of each epistemic state, LessEQA = {(!1 , !2 , i ) | (!1 , !2 ) 2 i }. Depending
2
P(·) is the powerset function.
27
On Using Model Checking for the Certification of Iterated Belief Changes
on whether a full change operator, a singular change, or another sub-problem is
considered, some special treatment is necessary.
For instance, consider the signature ⌃ = {a, b}, yielding the interpretations
⌦ = {ab, ab, ab, ab}. Moreover, consider the singular change C = ( 0 , ↵, 1 ),
where 0 = 0 is the total preorder treating every interpretation to be equally
plausible, i.e., ab =0 ab =0 ab =0 ab. Furthermore, let ↵ = a. The total preorder
1 = 1 treats all a-models to be equally plausible, but prefers them over all non
a-models, which are considered to be equally plausible, i.e., 1 is the unique total
preorder with ab =1 ab and ab <1 ab and ab =1 ab. We construct a structure AC
as follows: The universe is given by U AC = ⌦ [ { 0 , 1 } [ P(⌦). The predicates
and function symbols are interpreted according to Figure 2. The terms e0 and a
are interpreted as eA0
C
= 0 and aAC = Mod(↵).
In summary, the Certification-Problem of whether C satisfies (CR1) is
expressed as a model-checking problem for FOTPC , i.e., a change C satisfies
the postulate (CR1) if AC |= 'CR1 holds, where '(CR1) is the formula given in
Equation (4).
5 Implementation
We provide an implementation, called Alchourron, of the approach by combining
independent, self-developed Java libraries. Whereby the implementation consists
of two main parts: First, an implementation of the model-checking based approach
to the certification problem and its sub-problems and second, a user interface
realized via web-frontend.
Our implementation of the certification problem makes use of a domain
specific modelling of the area of iterated belief change. This contains the rep-
resentation of postulates, belief change operators and belief changes, and the
translation thereof into FOTPC -structures. The model-checking algorithm is
currently straight-forward and is part of an extensive institution-inspired imple-
mentation, called Logical Systems 3 , which allows representation and evaluation of
a variety of di↵erent logics in a unified way. Preconfigured postulates are stored
in TPTP syntax and parsed from there4 , mapping TPTP specified formula into
our internal representation. Some parts of the implementation are currently only
available upon request.
The user interface is publicly accessible by a web-frontend5 , which expands
on the previous work by Sauerwald and Haldimann [17]. The currently available
version allows the specification of a singular belief change using a browser-based
client. First, the user decides on a propositional signature for the language of
the belief change. Then a prior total preorder, an input formula, as well as the
posterior total preorder is entered. Figure 3 illustrates the belief change input.
After specifying the change, the web-interface allows the user to check whether
several preconfigured belief change postulates are satisfied. Optionally, a user
3
Sauerwald, K.: Logical Systems, 2021, github.com/Landarzar/logical-systems.
4
Steen, A.: Scala TPTP parser, 2021. DOI: 10.5281/zenodo.4672395.
5
Visit: https://www.fernuni-hagen.de/wbs/alchourron/
28
On Using Model Checking for the Certification of Iterated Belief Changes
Fig. 3: Input fields for the change from 0 to 1 by ↵ = a in Alchourron.
can also enter her own postulate by defining a first-order formula using FOTPC .
Formulas are described in TPTP syntax [24], e.g., the postulate (CR1) from
Section 4 can be expressed as follows:
! [W1,W2] : ((int(W1) & int(W2) & mod(W1, A) & mod(W2, A))
=> (lesseq(W1, W2, E0) <=> lesseq(W1, W2, op(E0, A))))
Internally, the user interface make use of a client-server architecture. In par-
ticular, postulate checking via compilation into a model-checking problem as
described in Section 4 is happening completely on the server side. The implemen-
tation is highly modularized, and we expect reusability of components for further
projects.
The client is implemented in TypeScript and utilizes the React framework.
Display of total preorders is provided by open-source web components6 that can
also represent ordinal conditional functions [23], which for instance implement
total preorders, but provide also more fine-grained representations of epistemic
states.
6 Empirical Evaluation and Improvements
We undertook measurements of the run-time for several predefined postulates and
belief changes. For the following, remember that the implementation computes the
answer to a given certification problem in three steps: The implementation has to
parse the request (including restoring the prior epistemic state and restoring pos-
terior epistemic states from a textual representation), build the FOTPC -structure
AC , and perform a FOTPC -model-check to determine whether or not the belief
change satisfies a postulate.
As the method for measuring the run-time, we used java.time.Instant,
while the server was running in a docker container. The same amount of resources
was provided for every run. To reduce variance, measurements were taken multiple
times and averaged. Even though concrete numbers depend on the system, overall
trends could be identified.
6
Heltweg, P.: Logic components, 2021. DOI: 10.5281/zenodo.4744650.
29
On Using Model Checking for the Certification of Iterated Belief Changes
106 |⌃| = 1
|⌃| = 2
105
Time (µs)
|⌃| = 3
104
103
102
es t tu r
e 2*
)
PR
) 5)
qu uc GM ( ( CR
e Re S tr (A ing n g
Pa
rs il d n g eck cki
Bu cki lC
h he
he de lC
el
C
Mo de
d Mo
Mo
Fig. 4: Average run-time for parsing, building a FOTPC -structure, and the FOTPC -model-
checking for the postulates (AGM2*), (PR) [4], and (CR5).
We obtained that the run-time is mainly dominated by the size of the signature.
Figure 4 presents prototypical results of the measurements. With respect to the
size of the signature, parsing the request, as well as building the initial structure
showed only small growth. Increasing the size of the signature from |⌃| = 1
to |⌃| = 3 increases the time needed to parse the request by a factor of ⇠1.4,
building AC took ⇠4.6 times as long. In contrast, the run-time for performing
model-checking of all considered postulates increased from 11978 µs for |⌃| = 1 to
12386828 µs (⇠12.4s) for |⌃| = 3, a factor of ⇠1034. For |⌃| = 3, most postulates
were checked in less than 100 milliseconds.
As special cases, consider the following postulates (CR5) and (CR6) from
Darwiche and Pearl [6]:
(CR5) if !1 , !3 |=↵ and !2 |=¬↵, then !3 < !1 and !2 !1 i↵ !2 ↵ !1
(CR6) if !1 , !3 |=↵ and !2 |=¬↵, then !3 < !1 and !2 < !1 i↵ !2 < ↵ !1
Each of the postulates (CR5) and (CR6) interrelate three worlds. Thus, when
modelling them in FOTPC , corresponding formulas quantify over three interpre-
tations.
One might note that the postulates with the high run-times are those which
contain three all-quantifiers (more than any other considered postulate). For
example for (CR5) and (CR6) we obtain the average run-times of 3161 ms and
3226 ms, respectively. We conclude that the number of quantifiers in a postulate
dominate the run-time. This coincides with theoretical results on the complexity
of first-order model-checking with respect to the quantifier rank [14].
The results gave rationale to change the implementation, such that all-
quantified formulas were now evaluated in parallel. This led to a speed-up of
30
On Using Model Checking for the Certification of Iterated Belief Changes
roughly factor two for individual postulates. In an additional step, the certification
of multiple postulates in one request was also done in parallel, allowing (CR5) and
(CR6) to be evaluated at the same time and not sequentially. After performance
optimizations, certification of a belief change for |⌃| = 3 was reduced from ⇠12.5
seconds to ⇠3.9 seconds, a speed-up factor of ⇠3.2.
7 Summary and Future Work
We proposed FOTPC , a first-order fragment to describe belief change postulates,
complemented with a methodology to construct a finite structure for a belief
change operator, employing total preorders as representation of epistemic states.
With this toolset, the certification of belief change operators can be understood as
a model-checking problem. We presented our implementation, which is available
online5 , as a proof of concept for our approach for singular belief changes. In
summary, we defined and formalized the certification problem and provided an
implementation thereof.
While this is only the first proposal, we expect that this approach will be highly
flexible regarding improvements and extensions. For future work we planning to
expand our approach in several directions. First, note that our implementation
of the model-checking-based certification already supports the certification of
complete belief change operators. However, the user interface is currently limited
to the certification of single-step changes. Thus, as a natural next step, we will
investigate ways to extend the web interface such that ultimately certification
of complete belief change operators is easily possible for users. Second, we are
planning to extend the whole approach to more complex representations of
epistemic states, e.g., ranking functions by Spohn [23]. Finally, we will improve
the efficiency of the implementation. This involves using a more sophisticated
and specialized method of first-order model-checking.
Acknowlegements
We would like to thank the reviewers for their fruitful and helpful comments. Kai
Sauerwald is supported by the Deutsche Forschungsgemeinschaft (DFG, German
Research Foundation) Grant BE 1700/10-1 awarded to Christoph Beierle as part
of the priority program ”Intentional Forgetting in Organizations” (SPP 1921).
The authors also thank Christoph Beierle for his helpful comments and support.
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. Booth, R.: On the logic of iterated non-prioritised revision. In: Kern-Isberner, G.,
Rödder, W., Kulmann, F. (eds.) Conditionals, Information, and Inference, Interna-
tional Workshop, WCII 2002, Hagen, Germany, May 13-15, 2002, Revised Selected
31
On Using Model Checking for the Certification of Iterated Belief Changes
Papers. Lecture Notes in Computer Science, vol. 3301, pp. 86–107. Springer (2002).
https://doi.org/10.1007/11408017 6
3. Booth, R., Fermé, E.L., Konieczny, S., Pino Pérez, R.: Credibility-limited improve-
ment operators. In: Schaub, T., Friedrich, G., O’Sullivan, B. (eds.) ECAI 2014 -
21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague,
Czech Republic. Frontiers in Artificial Intelligence and Applications, vol. 263, pp.
123–128. IOS Press (2014). https://doi.org/10.3233/978-1-61499-419-0-123
4. Booth, R., Meyer, T.A.: Admissible and restrained revision. J. Artif. Intell. Res.
26, 127–151 (2006)
5. Booth, R., Meyer, T.A., Wong, K.: A bad day surfing is better than a good day
working: How to revise a total preorder. In: Doherty, P., Mylopoulos, J., Welty,
C.A. (eds.) Proceedings, Tenth International Conference on Principles of Knowledge
Representation and Reasoning, Lake District of the United Kingdom, June 2-5,
2006. pp. 230–238. AAAI Press (2006)
6. Darwiche, A., Pearl, J.: On the logic of iterated belief revision. Artificial Intelligence
89, 1–29 (1997)
7. Fermé, E.L., Hansson, S.O.: AGM 25 years - twenty-five years of re-
search in belief change. J. Philosophical Logic 40(2), 295–331 (2011).
https://doi.org/10.1007/s10992-011-9171-9
8. Hild, M., Spohn, W.: The measurement of ranks and the laws
of iterated contraction. Artif. Intell. 172(10), 1195–1218 (2008).
https://doi.org/10.1016/j.artint.2008.03.002
9. Jin, Y., Thielscher, M.: Iterated belief revision, revised. Artif. Intell. 171(1), 1–18
(2007)
10. Katsuno, H., Mendelzon, A.O.: Propositional knowledge base revision and minimal
change. Artif. Intell. 52(3), 263–294 (1992)
11. Konieczny, S., Pino Pérez, R.: Improvement operators. In: Brewka, G., Lang, J.
(eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the
Eleventh International Conference, KR 2008, Sydney, Australia, September 16-19,
2008. pp. 177–187. AAAI Press (2008)
12. 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)
13. 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)
14. Libkin, L.: Elements of Finite Model Theory. Springer (2004)
15. Nayak, A.C., Pagnucco, M., Peppas, P.: Dynamic belief revision operators. Artif.
Intell. 146(2), 193–228 (2003)
16. Nebel, B.: How Hard is it to Revise a Belief Base?, pp. 77–145. Springer Netherlands,
Dordrecht (1998). https://doi.org/10.1007/978-94-011-5054-5 3
17. Sauerwald, K., Haldimann, J.: WHIWAP: checking iterative belief changes. In:
Beierle, C., Ragni, M., Stolzenburg, F., Thimm, M. (eds.) Proceedings of the
8th Workshop on Dynamics of Knowledge and Belief (DKB-2019) and the 7th
Workshop KI & Kognition (KIK-2019), Kassel, Germany, September 23, 2019.
CEUR Workshop Proceedings, vol. 2445, pp. 14–23. CEUR-WS.org (2019), http:
//ceur-ws.org/Vol-2445/paper 2.pdf
32
On Using Model Checking for the Certification of Iterated Belief Changes
18. Sauerwald, K., Heltweg, P., Beierle, C.: Certification of iterated belief changes via
model checking and its implementation. In: Amgoud, L., Booth, R. (eds.) 19th
International Workshop on Non-Monotonic Reasoning (NMR 2021), Hanoi, Vietnam,
November 2-5, 2021, Proceedings (2021), (forthcoming)
19. Sauerwald, K., Kern-Isberner, G., Beierle, C.: A conditional perspective for iterated
belief contraction. In: Giacomo, G.D., Catalá, A., Dilkina, B., Milano, M., Barro, S.,
Bugarı́n, A., Lang, J. (eds.) ECAI 2020 - 24nd European Conference on Artificial
Intelligence, August 29th - September 8th, 2020, Santiago de Compostela, Spain.
pp. 889–896. IOS Press (2020)
20. Schwind, N., Konieczny, S., Lagniez, J., Marquis, P.: On computational aspects
of iterated belief change. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth
International Joint Conference on Artificial Intelligence, IJCAI 2020. pp. 1770–1776
(2020). https://doi.org/10.24963/ijcai.2020/245
21. Schwind, N., Konieczny, S., Marquis, P.: On belief promotion. In: Thielscher, M.,
Toni, F., Wolter, F. (eds.) Principles of Knowledge Representation and Reasoning:
Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona,
30 October - 2 November 2018. pp. 297–307. AAAI Press (2018), https://aaai.org/
ocs/index.php/KR/KR18/paper/view/18025
22. Schwind, N., Konieczny, S.: Non-Prioritized Iterated Revision: Improvement via
Incremental Belief Merging. In: Proceedings of the 17th International Conference
on Principles of Knowledge Representation and Reasoning. pp. 738–747 (9 2020).
https://doi.org/10.24963/kr.2020/76, https://doi.org/10.24963/kr.2020/76
23. Spohn, W.: Ordinal conditional functions: a dynamic theory of epistemic states. In:
Harper, W., Skyrms, B. (eds.) Causation in Decision, Belief Change, and Statistics,
II, pp. 105–134. Kluwer Academic Publishers (1988)
24. Sutcli↵e, G.: The TPTP Problem Library and Associated Infrastructure. From CNF
to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), 483–502 (2017)
25. Turán, G., Yaggie, J.: Characterizability in belief revision. In: Proceedings of the
Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015,
Buenos Aires, Argentina, July 25-31, 2015. pp. 3236–3242 (2015)
33