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

Abstract

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.

References in corpus (2)

• Achieving while maintaining: A logic of knowing how with intermediate constraints
• Uncertainty-Based Semantics for Multi-Agent Knowing How Logics