  Logic programs with aggregates (LPA) are one of the major linguistic
extensions to Logic Programming (LP). In this work, we propose a generalization
of the notions of unfounded set and well-founded semantics for programs with
monotone and antimonotone aggregates (LPAma programs). In particular, we
present a new notion of unfounded set for LPAma programs, which is a sound
generalization of the original definition for standard (aggregate-free) LP. On
this basis, we define a well-founded operator for LPAma programs, the fixpoint
of which is called well-founded model (or well-founded semantics) for LPAma
programs. The most important properties of unfounded sets and the well-founded
semantics for standard LP are retained by this generalization, notably
existence and uniqueness of the well-founded model, together with a strong
relationship to the answer set semantics for LPAma programs. We show that one
of the D-well-founded semantics, defined by Pelov, Denecker, and Bruynooghe for
a broader class of aggregates using approximating operators, coincides with the
well-founded model as defined in this work on LPAma programs. We also discuss
some complexity issues, most importantly we give a formal proof of tractable
computation of the well-founded model for LPA programs. Moreover, we prove that
for general LPA programs, which may contain aggregates that are neither
monotone nor antimonotone, deciding satisfaction of aggregate expressions with
respect to partial interpretations is coNP-complete. As a consequence, a
well-founded semantics for general LPA programs that allows for tractable
computation is unlikely to exist, which justifies the restriction on LPAma
programs. Finally, we present a prototype system extending DLV, which supports
the well-founded semantics for LPAma programs, at the time of writing the only
implemented system that does so. Experiments with this prototype show
significant computational advantages of aggregate constructs over equivalent
aggregate-free encodings.
