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.

翻译：目标导向知道如何的逻辑在标准认知逻辑的基础上扩展了一个知道如何算子。知道如何算子被解释为存在一个策略，使得智能体知道该策略能够确保p成立。本文针对多智能体版本的策略知道如何的逻辑提出了一种表列法程序，并证明了该表列法程序的可靠性和完备性。本文还证明了该逻辑的可满足性问题可在PSPACE中判定。