Note: An extended version of this paper has been published at the 7th Workshop on Formal and Cognitive Reasoning, you can find it here.

Our paper “Certification of Iterated Belief Changes via Model Checking and its Implementation” got accepted to the 19th International Workshop on Non-Monotonic Reasoning (NMR-2021) at the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 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

Iterated belief change investigates principles for changes on epistemic states and their representational groundings. 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 present 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.