Partenaires

CNRS
Université d'Artois IUT de Lens



retour à l'accueil

Home page > Research > Old seminars > T. de Lima (CRIL, Univesité d’Artois) - A tableaux method for public announcement logic

T. de Lima (CRIL, Univesité d’Artois) - A tableaux method for public announcement logic

Abstract: Public announcement logic extends multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. In this talk, I will present a labelled tableau calculus for this logic. It decides satisfiability of formulas in deterministic polynomial space. Since this problem is known to be PSPACE-complete, it follows that such proof method is optimal.

In the same section :