By our construction, pn ∈ Un, and so Un ∩ X 6= ∅. Therefore X does not admit any P-proof scheme for p. Thus p /∈ GLP (X) = GLP (Sn∈N Xn). But this would contradict our assumption that GLP is upper-half continuous. Thus there can be no such p and hence P must be a FSP-program. ✷

## 5 Extensions To Cc -Programs

In [SNS02] Niemel¨a and coauthors defined a significant extension of logic programming with stable semantics which allows for programming with cardinality constraints, and, more generally, with weight constraints. This extension has been further studied in [MR04, MNT07]. To keep things simple, we will limit our discussion to cardinality constraints only, although it is possible to extend our arguments to any class of convex constraints [LT05]. *Cardinality constraints* are expressions of the form lXu, where **l, u** ∈ N, l ≤ u and X is a finite set of atoms. The semantics of an atom lXu is that a set of atoms M satisfies kXl if and only if k ≤ |M ∩ X|. When l = 0, we do not write it, and, likewise, when u ≥ |X|, we omit it, too. Thus an atom p has the same meaning as 1{p} while ¬p has the same meaning as {p}0.

The stable semantics for CC -programs is defined via fixpoints of an analogue of the Gelfond-Lifschitz operator GLP ; see the details in [SNS02] and [MR04]. The operator in question is neither monotone nor antimonotone. But when we limit our attention to the programs P where clauses have the property that the head consists of a single atom (i.e. are of the form 1{p}), then one can define an operator CCGLP which is antimonotone and whose fixpoints are stable models of P. This is done as follows.

Given a clause C
$$p\leftarrow l_{1}X_{1}u_{1},\ldots,l_{m}X_{m}u_{m},$$
we transform it into the clause
$p\gets l_{1}X_{1},\ldots,l_{m}X_{m},X_{1}u_{1},\ldots,X_{m}u_{m}$  $\bullet$\(\bullet
[MNT07]. We say that a clause C of the form (4) is a CC -Horn clause if it is of the form p ← l1X1**, . . . , l**mXm. (5)
A CC -Horn program is a CC -program all of whose clauses are of the form (5). If P is a CC -Horn program, we can define the analogue of the one step provability operator TP by defining that for a set of atom M,
TP (M) = {p : (∃C = p ← l1X1, . . . , lmXm)(∀i ∈ {1, . . . m})(|Xi ∩ M| ≥ li)}
(6)

$\ensuremath{\mathcal{A}}$