In this paper we show that an arbitrary propositional theory, when interpreted under the answer sets semantics (called Equilibrium Logic for this general syntax), 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 trasnformation, and one that constructs a program starting from the countermodels of the theory in the intermediate logic of here-and-there.

PDF

Theory and Practice of Logic Programming, Vol. 7 (2007), pp. 745-759.

@journal{cab07, title={Propositional Theories are Strongly equivalent to Logic Programs}, author={Pedro Cabalar and Paolo Ferraris}, volume={7}, journal={Theory and Practice of Logic Programming}, pages={745-759}, url="http://www.cs.utexas.edu/users/ai-lab?cab07", year={2007} }