Abstract: In this paper, we propose a decidable single-agent modal logic for reasoning about goal-directed “knowing how”, based on ideas from linguistics, philosophy, modal logic, and automated planning in AI. We first define a modal language to express “I know how to guarantee (Formula presented.) given (Formula presented.)” with a semantics based not on standard epistemic models but on labeled transition systems that represent the agent’s knowledge of his own abilities. The semantics is inspired by conformant planning in AI. A sound and complete proof system is given to capture valid reasoning patterns, which highlights the compositional nature of “knowing how”. The logical language is further extended to handle knowing how to achieve a goal while maintaining other conditions.
(This is an extended journal version of the LORI2015 paper)