Tableaux for Single-Agent Epistemic PDL with Perfect Recall and No Miracles

Epistemic propositional dynamic logic (EPDL) is a combination of epistemic logic and propositional dynamic logic. The properties, perfect recall and no miracles, capture the interactions between actions and knowledge. In this paper, we present a tableau-based decision procedure for deciding satisfiability of single-agent EPDL with perfect recall and no miracles. We prove the soundness and completeness of the tableau procedure with respect to models with perfect recall and no miracles.EICPCI-S(ISTP)Y.J.Li@rug.nl230-242939