On the Continuity of Gelfond-Lifschitz Operator and Other Applications of Proof-Theory in ASP

Using a characterization of stable models of logic programs P as satisfying valuations of a suitably chosen propositional theory, called the set of reduced defining equations r Phi(P), we show that the finitary character of that theory r Phi(P) is equivalent to a certain continuity property of the Gelfond-Lifschitz operator GL(P) associated with the program P. The introduction of the formula r Phi(P), leads to a double-backtracking algorithm for computation of stable models by reduction to satisfiability of suitably chosen propositional theories. This algorithm does not use the reduction via loop-formulas as proposed in [1] or its extension proposed in [2]. Finally, we discuss possible extensions of techniques proposed in this paper to the context of cardinality constraints.