Journal of the Association for Computing Machinery, Vol. 42, No. 2, March 1995, pp. 421–457.

NP Trees and Carnap’s Modal Logic

GEORG GOTTLOB

Abstract. In this paper we consider problems and complexity classes definable by interdependent queries to an oracle in NP. How the queries depend on each other is specified by a directed graph G. We first study the class of problems where G is a general dag and show that this class coincides with Δ_{2}^{P}. We then consider the class where G is a tree. Our main result states that this class is identical to P^{NP}[O(log n)], the class of problems solvable in polynomial time with a logarithmic number of queries to an oracle in NP. This result has interesting applications in the fields of modal logic and artificial intelligence. In particular, we show that the following problems are all P^{NP}[O(log n)] complete: validity-checking of formulas in Carnap’s modal logic, checking whether a formula is almost surely valid over finite structures in modal logics K, T, and S4 (a problem recently considered by Halpern and Kapron [1992]), and checking whether a formula belongs to the stable set of beliefs generated by a propositional theory.

We generalize the case of dags to the case where G is a general (possibly cyclic) directed graph of NP-oracle queries and show that this class corresponds to Π_{2}^{P}. We show that such graphs are easily expressible in autoepistemic logic. Finally, we generalize our complexity results to higher classes of the polynomial-time hierarchy.

Categories and Subject Descriptors. F.1.2[relations among complexity classes]; F.2.2[Complexity of proof procedures; computations on discrete structures]; F.4.1[Computational logic]; I.2.3[Nonmonotonic reasoning and belief revision]; I.2.4

General Terms. Theory

Additional Key words and Phrases. Autoepistemic logic, bounded query computation, epistemic logic, modal logic, NP, oracle, trees

Copyright 1995 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.