We investigate the complexity of the satisfiability problem for a modal logic expressing `knowing how' assertions, related to an agent's abilities to achieve a certain goal. We take one of the most standard semantics for this kind of logics based on linear plans. Our main result is a proof that checking satisfiability of a `knowing how' formula can be done in $\Sigma_2^P$. The algorithm we present relies on eliminating nested modalities in a formula, and then performing multiple calls to a satisfiability checking oracle for propositional logic.

翻译：我们研究了表达“知道如何做到”断言的模态逻辑的可满足性问题的复杂性，该逻辑与主体实现特定目标的能力相关。我们采用了基于线性计划的此类逻辑最标准语义之一。我们的主要结果是证明检查“知道如何做到”公式的可满足性可以在 $\Sigma_2^P$ 内完成。我们提出的算法依赖于消除公式中的嵌套模态，然后多次调用命题逻辑的可满足性检查预言机。