Proof theory of epistemic logic of programs

Paolo Maffezioli, Alberto Naibo

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Scopus)
792 Downloads (Pure)


A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to give a step-by-step reconstruction of agents omniscience. In particular, its semantic assumptions are made explicit and a possible solution can be found in weakening the properties of the knowledge operator.
Original languageEnglish
Pages (from-to)301-328
Number of pages26
JournalLogic and Logical Philosophy
Issue number3
Early online date12-Sept-2013
Publication statusPublished - Sept-2014


  • epistemic logic
  • dynamic propositional logic
  • structural proof theory
  • labelled sequent calculus
  • epistemic paradox

Cite this