Tableaux for the Logic of Strategically Knowing How
This work provides a formal method for verifying strategic knowledge in multi-agent systems, which is incremental as it extends existing epistemic logic frameworks.
The paper tackles the problem of automated reasoning for a multi-agent logic of strategically knowing-how by presenting a tableau procedure, proving its soundness and completeness, and showing that the satisfiability problem is decidable in PSPACE.
The logic of goal-directed knowing-how 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 p. 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.