Computational properties of epistemic logic programs

Gelfond's epistemic logic programs are not only an extension of disjunctive extended logic programs for handling difficulties in reasoning with incomplete information, but also an effective formalism to represent agents'epistemic reasoning under a logic programming setting. Recently there is an increasing research in this direction. However, for many years the complexity of epistemic logic programs remains unclear. This paper provides a precise answer to this problem. We prove that consistency check for epistemic logic programs is in PSPACE and this upper bound is also tight. The approach developed in our proof is of interest on its own: it immediately yields an algorithm to compute world views of an epistemic logic program, and it can also be used to study computational properties of nested epistemic logic programs - a significant generalization of Gelfond's formalism.