Advertisement
Published in:
2008 | OriginalPaper | Chapter
On the Continuity of Gelfond-Lifschitz Operator and Other Applications of Proof-Theory in ASP
Authors : V. W. Marek, J. B. Remmel
Published in: Logic Programming
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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
${\mathit{GL}}_P$
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.