Finitary S5-theories

Abstract

The objective of this paper is to identify a class of epistemic logic theories with group knowledge operators which have the fundamental property of being characterized by a finite number of finite models (up to equivalence). We specifically focus on S5-theories. We call this class of epistemic logic theories as finitary S5-theories. Models of finitary S5-theories can be shown to be canonical in that they do not contain two worlds with the same interpretation. When the theory is pure, these models are minimal and differ from each other only in the actual world. The paper presents an algorithm for computing all models of a finitary S5-theory. Finitary S5-theories find applications in several contexts—in particular, the paper discusses their use in epistemic multi-agent planning.