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 Sigma(P)(2). 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.