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. (shrink)

Larry Moss and Rohit Parikh used subset semantics to characterize a family of logics for reasoning about knowledge. An important feature of their framework is that subsets always decrease based on the assumption that knowledge always increases. We drop this assumption and modify the semantics to account for logics of knowledge that handle arbitrary changes, that is, changes that do not necessarily result in knowledge increase, such as the update of our knowledge due to an action. We present a system (...) which is complete for subset spaces and prove its decidability. (shrink)

is used to give a formalization of Artemov’s knowledge based reasoning approach to game theory, (KBR), [ 4 , 5 ]. Epistemic states of players are represented explicitly and reasoned about formally. We give a detailed analysis of the Centipede game using both proof theoretic and semantic machinery. This helps make the case that PDL + E can be a useful basis for the logical investigation of game theory.