Our paper “On Using Model Checking for the Certification of Iterated Belief Changes” got accepted to the 7th Workshop on Formal and Cognitive Reasoning (FCR-2021) at the 44th German Conference on Artificial Intelligence (KI-2021). During the workshop I held a short presentation of the results. You can find both the paper as well as the presentation slides here.
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.