On the decidability and complexity of reasoning about only knowing

We study reasoning in Levesque's logic of only knowing. In particular, we first prove that extending a decidable subset of first-order logic with the ability of reasoning about only knowing preserves decidability of reasoning, as long as quantifying-in is not allowed in the language, and define a general method for reasoning about only knowing in such a case. Then, we show that the problem of reasoning about only knowing in the propositional case Lies at the second level of the polynomial hierarchy. Thus, it is as hard as reasoning in the majority of propositional formalisms for nonmonotonic reasoning, like default logic, circumscription, and autoepistemic logic, and it is easier than reasoning in propositional formalisms based on the minimal knowledge paradigm, which is strictly related to the notion of only knowing. Finally, we identify a syntactic restriction in which reasoning about only knowing is easier than in the general propositional case, and provide a specialized deduction method for such a restricted setting. (C) 2000 Elsevier Science B.V. All rights reserved