Sesión especial del Seminario (10-4-2011): Tiago de Lima

Fecha / Date: 10-4-2011.

Hora / Time: 10:00 h.

Lugar / Location: Aula 213 de la Facultad de Filología - Universidad de Sevilla.

Ponente / Lecturer: Tiago de Lima.

Título / Tittle: A tableaux method for public announcement logic.

Resumen / 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 logic, one may write, e.g., formulae of the form [p ∧ q]Ki p, which mean ‘after the announcement of p ∧ q, the consequence p is known by agent i’. In this talk, I will present this logic and also a labelled tableaux method for satisfiability checkin of formulae. The main attention is given to the explanation of the tableaux rules, bu some discussion about its soundness, completeness, termination, and computational complexity will also be addressed.