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Øp, we show that the finitary character of that theory rØp is equivalent to a certain continuity property of the Gelfond-Lifschitz operator GLp associated with the program P. The introduction of the formula rØ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.