28 February 2007, Logic Tea, Tiago de Lima

Abstract

Public announcement logic (PAL) is an extension of multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. It is one from a series of logics developed with the aim of modelling dynamics of knowledge and belief in multi-agent settings. Being the simplest form of agent communication, public announcements are present in all of these logics.

The well-known proof system for PAL is obtained by means of reduction axioms. They define a truth preserving translation from PAL to epistemic logic. It thus follows that both logics have the same expressivity, but the translation is exponential. However, when positive introspection is admitted, satisfiability in PAL is indeed PSPACE-complete.

We present a tableau-calculus for public announcement logics with and without positive introspection. The method does not translate PAL-formulas to other languages and therefore decides satisfiability by constructing a model for the original formula. In addition, it turns to be optimal in unrestricted and reflexive models.

The Logic Tea homepage can be found at http://www.illc.uva.nl/logic_tea/. For more information, please contact Jonathan Zvesper (jonathan at illc.uva.nl), Hartmut Fitz (h.fitz at uva.nl) or Joel Uckelmann (juckelma at science.uva.nl).