We study properties of programs with monotone and convex constraints. We extend to these formalisms concepts and results from normal logic programming. They include the notions of strong and uniform equivalence with their characterizations, tight programs and Fages Lemma, program completion and loop formulas. Our results provide an abstract account of properties of some recent extensions of logic programming with aggregates, especially the formalism of lparse programs. They imply a method to compute stable models of lparse programs by means of off-the-shelf solvers of pseudo-boolean constraints, which is often much faster than the smodels system.
p04 and pdb06 studied a more general class of aggregates and developed a systematic theory of aggregates in logic programming based on the approximation theory @cite_0 . The resulting theory covers not only the stable models semantics but also the supported-model semantics and extensions of 3-valued Kripke-Kleene and well-founded semantics. The formalism introduced and studied by p04 and pdb06 allows for arbitrary aggregates (not only monotone ones) to appear in the bodies of rules. However, it does not allow for aggregates to appear in the heads of program clauses. Due to differences in the syntax and the scope of semantics studied there is no simple way to relate p04 and pdb06 formalism to programs with monotone (convex) constraints. We note though that programs with abstract monotone constraints with the heads of rules of the form @math can be viewed almost literally as programs in the formalism by p04 and pdb06 and that they have the same stable models according to the definitions we used in this paper and those by p04 and pdb06 .
@cite_0
1598820892
In this paper, we propose an extension of the well-founded and stable model semantics for logic programs with aggregates. Our approach uses Approximation Theory, a fixpoint theory of stable and well-founded fixpoints of non-monotone operators in a complete lattice. We define the syntax of logic programs with aggregates and define the immediate consequence operator of such programs. We investigate the well-founded and stable semantics generated by Approximation Theory. We show that our approach extends logic programs with stratified aggregation and that it correctly deals with well-known benchmark problems such as the shortest path program and the company control problem.