How Easy it is to Know How: An Upper Bound for the Satisfiability Problem

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 ${\mathrm{\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.