Finitary S5-theories

Tran Cao Son, Enrico Pontelli, Chitta Baral, Gregory Gelfond

Research output: Contribution to journalArticlepeer-review

13 Scopus citations


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.

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Finitary S5-theories'. Together they form a unique fingerprint.

Cite this