Propositional theories are strongly equivalent to logic programs

TL;DR

This paper demonstrates that any propositional theory under answer set semantics can be equivalently expressed as a disjunctive logic program, enhancing understanding of their relationship and translation methods.

Contribution

It proves that propositional theories are strongly equivalent to disjunctive logic programs, providing two different methods for the translation.

Findings

Any propositional theory can be reexpressed as a strongly equivalent disjunctive logic program.

Two proofs are provided: a syntactic transformation and a model-based construction.

The result bridges propositional theories and logic programming under answer set semantics.

Abstract

This paper presents a property of propositional theories under the answer sets semantics (called Equilibrium Logic for this general syntax): any theory can always be reexpressed as a strongly equivalent disjunctive logic program, possibly with negation in the head. We provide two different proofs for this result: one involving a syntactic transformation, and one that constructs a program starting from the countermodels of the theory in the intermediate logic of here-and-there.