Tableaux for the Logic of Strategically Knowing How

The logic of goal-directed knowing how proposed in [5] extends the standard epistemic logic with an operator of knowing how. The knowing how operator is interpreted as that there exists a strategy such that the agent knows that the strategy can make sure that phi. This paper presents a tableau procedure for the multi-agent version of the logic of strategically knowing how and shows the soundness and completeness of this tableau procedure. This paper also shows that the satisfiability problem of the logic can be decided in PSPACE.