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 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 attention, 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 FO TPC , 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 FO TPC -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 [18] by an empirical evaluation.
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:
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 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.
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?
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.
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 symbols denoted by FO TPC (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 FO TPC 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)! (Mod(w, x)!Mod(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]:
In FO TPC , we address this by reserving e 0 and a as special terms, where e 0 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:
This could be expressed in FO TPC by the following formula ' CR1 :
! (LessEQ(w 1 , w 2 , e 0 ) $ LessEQ(w 1 , w 2 , op(e 0 , a)))
Universe We describe now how objects like belief change operators, singular changes and so on are related to FO TPC formulas.
Encoding as Model-Checking. Internally, we use the standard truth-functional semantics of first-order logic for FO TPC . 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, Int A = ⌦, and LessEQ allows access to the total preorder of each epistemic state,
Depending 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 A C as follows: The universe is given by
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 FO TPC -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 [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 can also enter her own postulate by defining a first-order formula using FO TPC . Formulas are described in TPTP syntax [24], e.g., the postulate (CR1) from Section 4 can be expressed as follows:
=> (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 [23], which for instance implement total preorders, but provide also more fine-grained representations of epistemic states.
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 FO TPC -structure A C , and perform a FO TPC -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. 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 A C 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]:
Each of the postulates (CR5) and (CR6) interrelate three worlds. Thus, when modelling them in FO TPC , corresponding formulas quantify over three interpretations.
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 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.
We proposed FO TPC , 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 online 5 , 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 e ciency of the implementation. This involves using a more sophisticated and specialized method of first-order model-checking.
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.