In this paper, we present a framework for the semantics and the computation of aggregates in the context of logic programming. In our study, an aggregate can be an arbitrary interpreted second order predicate or function. We define extensions of the Kripke-Kleene, the well-founded and the stable semantics for aggregate programs. The semantics is based on the concept of a three-valued immediate consequence operator of an aggregate program. Such an operator approximates the standard two-valued immediate consequence operator of the program, and induces a unique Kripke-Kleene model, a unique well-founded model and a collection of stable models. We study different ways of defining such operators and thus obtain a framework of semantics, offering different trade-offs between precision and tractability. In particular, we investigate conditions on the operator that guarantee that the computation of the three types of semantics remains on the same level as for logic programs without aggregates. Other results show that, in practice, even efficient three-valued immediate consequence operators which are very low in the precision hierarchy, still provide optimal precision.
A novel feature of the language of weight constraints was that it allows weight constraints to be present also in the head of the rules. This approach have been further developed in different directions. One line of research was to consider different variations and extensions of weight constraints like abstract constraints @cite_23 , monotone cardinality atoms @cite_10 or set constraints @cite_20 . Such constraint atoms correspond in a natural way to aggregate atoms. The stable semantics of these extensions is also defined in terms of lattice operators. However, since constraint atoms are allowed in the heads of rules, the operators become non-deterministic and the algebraic theory is quite different than the approximation theory we used in this work. However, all the semantics agree on the class of definite aggregate programs and its least model semantics. The equivalent of a definite logic program in @cite_20 is called a Horn SC-logic programs and such programs are also characterized by a unique model which is the least fixpoint of a deterministic monotone operator @math which is the equivalent of our @math operator.
@cite_20 @cite_10 @cite_23
1540263588 1638553575 1854994931
We investigate a generalization of weight-constraint programs with stable semantics, as implemented in the ASP solver smodels. Our programs admit atoms of the form ( X, F ) where X is a finite set of propositional atoms and ( F ) is an arbitrary family of subsets of X. We call such atoms set constaints and show that the concept of stable model can be generalized to programs admitting set constraints both in the bodies and the heads of clauses. Natural tools to investigate the fixpoint semantics for such programs are nondeterministic operators in complete lattices. We prove two fixpoint theorems for such operators. We investigate mca-programs, that is, logic programs with clauses built of monotone cardinality atoms of the form kX, where k is a non-negative integer and X is a finite set of propositional atoms. We develop a theory of mca-programs. We demonstrate that the operational concept of the one-step provability operator generalizes to mca-programs, but the generalization involves nondeterminism. Our main results show that the formalism of mca-programs is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with cardinality atoms and with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue. We propose and study extensions of logic programming with constraints represented as generalized atoms of the form C(X), where X is a finite set of atoms and C is an abstract constraint (formally, a collection of sets of atoms). Atoms C(X) are satisfied by an interpretation (set of atoms) M, if M ∩ X ∈ C. We focus here on monotone constraints, that is, those collections C that are closed under the superset. They include, in particular, weight (or pseudo-boolean) constraints studied both by the logic programming and SAT communities. We show that key concepts of the theory of normal logic programs such as the one-step provability operator, the semantics of supported and stable models, as well as several of their properties including complexity results, can be lifted to such case.