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