%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "gottlob95a.ltx",
%%%     date      = "20 November 1995",
%%%     time      = "21:41:33 EST",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "05945 116 539 4413",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 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.
%%%                  
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{Gottlob95a}

\title{{NP} Trees and {Carnap's} Modal Logic}

\author{Georg Gottlob}

\Pages{421--457}

\Month{March}

\Year{1995}

\Volume{42}

\Number{2}

\maketitle

\begin{abstract}

In this paper we consider problems and complexity classes definable by
  interdependent queries to an oracle in $\mathbf{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 $\Delta^P_2$. We then consider the class where $G$ is a tree. Our main
  result states that this class is identical to $\mathbf{P}^{\mathbf{NP}}
  [O(\log n)]$, the class of problems solvable in polynomial time with a
  logarithmic number of queries to an oracle in $\mathbf{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
  $\mathbf{P}^{\mathbf{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 $\mathbf{K}$, $\mathbf{T}$, and
  $\mathbf{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. \par We generalize the case of dags to the case
  where $G$ is a general (possibly cyclic) directed graph of
  $\mathbf{NP}$-oracle queries and show that this class corresponds to
  $\mathbf{\Pi}^P_2$. 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.

\end{abstract}

\begin{categories}

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

\end{categories}

\begin{terms}

Theory

\end{terms}

\begin{keywords}

Autoepistemic logic, bounded query computation, epistemic logic, modal logic,
  NP, oracle, trees

\end{keywords}

\end{document}
