Characterising equilibrium logic and nested logic programs: Reductions and complexity,

Equilibrium logic is an approach to non-monotonic reasoning that extends the stable-model and answer-set semantics for logic programs. In particular, it includes the general case ofnested 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 intoquantified propositional logic, an extension of classical propositional logic where quantifications over atomic formulas are permitted. Thus, quantified propositional logic is a fragment of second-order logic, and its formulas are usually referred to asquantified Boolean formulas(QBFs). 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 QBF such that the latter is valid precisely in case the former holds. The basic tasks we deal with here are theconsistency problem,brave reasoningandskeptical reasoning. Additionally, we also provide encodings for testing equivalence of theories or programs under different notions of equivalence, viz.ordinary,stronganduniform equivalence. For all considered reasoning tasks, we analyse their computational complexity and give strict complexity bounds. Hereby, our encodings yield upper bounds in a direct manner. Besides this useful feature, our approach has the following benefits: First, our encodings yield auniform axiomatisationfor a variety of problems in a common language. Second, extant solvers for QBFs can be used as back-end inference engines to realise implementations of the encoded task in a rapid prototyping manner. Third, our axiomatisations also allow us to straightforwardly relate equilibrium logic with circumscription.