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 FOTPCstructure. 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.
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 [
The research on (iterated) belief change is focussed on propositional logic (but
not limited to). Often, total preorders over interpretations [
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
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. [
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
attention, notable exceptions are results about the complexity for specific operations
[
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 modelchecking 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 [
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 [
↵ =
Here (sAGM5es*) is a stronger version of the extensionality postulate from the
revision approach by Alchourr´on, G¨ardenfors and Makinson [
The framework by Darwiche and Pearl is di↵erent from the classical setup for
belief revision theory by AGM [
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 [
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 [
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 – A sequence of belief changes 1 ↵ 1 = 2, and 2 ↵ 2 = – All singular belief changes on a state , i.e. the set {( 1, ↵, ↵ = 0 hold? 3, and . . . 2) 2 | = 1}
In the next section we present a model-checking based formalisation of the Certification-Problem. 4
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. [
LessEQ(w1, w2, e) w1 w2 in e Int(w) w is an interpretation ES(e) e is an epistemic state F orm(a) a is a formula Function op(e0, a) or(a, b) not(a)
op(e0, a) is a result of changing e0 by a propositional disjunction propositional negation
! 2 Mod( ), ! 2 Mod(↵ ) !1 !2 ! 2 ⌦
2 E ↵ 2 L Exemplary appearance Bel(
↵ = 0 (↵ _ )) = . . . ¬↵ /2 Bel( ↵ ) 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):=8 w.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 [
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, !22 Mod(↵ ), then !1 !2 , !1 ↵ !2 This could be expressed in FOTPC by the following formula 'CR1: 'CR1 = 8 w1, w2. (Int(w1) ^ Int(w2) ^ M od(w1, a) ^ M od(w2, a)) ! (LessEQ(w1, w2, e0) $ LessEQ(w1, w2, op(e0, a)))
U AC = ⌦ [ {
0, 1} [ P (⌦ ) Predicates
M odAC = {(!, x) | x 2 P (⌦ ) [ {
IntAC = ⌦
ESAC = { 0, 1}
F ormAC = P(⌦ ) LessEQAC = {(!1, !2, i) | !1 i !2} Functions orAC = ↵ 1, ↵ 2. ↵ 1 [ ↵ 2 notAC = ↵ 1. ⌦ \ ↵ 1 opAC = ({( , , ) | 2 P (⌦ ), 2 { 0, 1}, ! 2 Mod(x)}} eAC = 0 0 aAC = Mod(↵ ) 0, 1}} \ {( 0, ↵, 0}) [ { ( 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 [
Bel(a, e) := (F orm(a) ^ ES(e)) ! (8 x.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 insensitive 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. 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 e0AC = 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
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 representation 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 implementation, called Logical Systems3, 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 [
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/
can also enter her own postulate by defining a first-order formula using FOTPC.
Formulas are described in TPTP syntax [
=> (lesseq(W1, W2, E0) <=> lesseq(W1, W2, op(E0, A))))
Internally, the user interface make use of a client-server architecture. In particular, postulate checking via compilation into a model-checking problem as described in Section 4 is happening completely on the server side. The implementation 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 [
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 posterior 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. 106 )s 105 µ ( e im 104 T 103 102
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 [
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 [
The results gave rationale to change the implementation, such that allquantified formulas were now evaluated in parallel. This led to a speed-up of 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
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 [
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.