Tableaux for a combination of propositional dynamic logic and epistemic logic with interactions

摘要

Epistemic prepositional dynamic logic (EPDL) is a combination of epistemic logic and prepositional dynamic logic. Two properties, perfect recall and no miracles, capture the interactions between actions and knowledge. In this article, we present a tableau-based decision procedure for deciding the satisfiability of single-agent EPDL formula in models with perfect recall and no miracles.