  Equilibrium logic is an approach to nonmonotonic reasoning that extends the
stable-model and answer-set semantics for logic programs. In particular, it
includes the general case of nested logic programs, where arbitrary Boolean
combinations are permitted in heads and bodies of rules, as special kinds of
theories. In this paper, we present polynomial reductions of the main reasoning
tasks associated with equilibrium logic and nested logic programs into
quantified propositional logic, an extension of classical propositional logic
where quantifications over atomic formulas are permitted. We provide reductions
not only for decision problems, but also for the central semantical concepts of
equilibrium logic and nested logic programs. In particular, our encodings map a
given decision problem into some formula such that the latter is valid
precisely in case the former holds. The basic tasks we deal with here are the
consistency problem, brave reasoning, and skeptical reasoning. Additionally, we
also provide encodings for testing equivalence of theories or programs under
different notions of equivalence, viz. ordinary, strong, and uniform
equivalence. For all considered reasoning tasks, we analyse their computational
complexity and give strict complexity bounds.
