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

C. Areces, V. Cassano, P. Castro, R. Fervari, and A. Saravia. How Easy it is to Know How: An Upper Bound for the Satisfiability Problem. In S. Gaggl, M. Martinez, and M. Ortiz, editors, Logics in Artificial Intelligence. 18th European Conference, JELIA 2023, Dresden, Germany, September 20–22, 2023, Proceedings, Lecture Notes in Computer Science, pp. 405–419, 2023.

Download

[pdf] 

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 $Σ_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.

BibTeX

@InCollection{arec:howe23,
  author =       "C. Areces and V. Cassano and P. Castro and R. Fervari
                 and A. Saravia",
  title =        "How Easy it is to Know How: An Upper Bound for the
                 Satisfiability Problem",
  editor = {S. Gaggl and M. Martinez and M. Ortiz},
  booktitle =    "Logics in Artificial Intelligence.  18th European
                  Conference, JELIA 2023, Dresden, Germany, September
                  20–22, 2023, Proceedings",
  ISBN = {978-3-031-43618-5},
  pages = {405--419},
  series = {Lecture Notes in Computer Science},
  year =         "2023",
  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 $Σ_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.",
}