It is easy to see that TP is monotone operator that the least fixed point of TP is
given by
$$l f p(T_{P})=\bigcup_{n\geq0}T_{P}^{n}(\varnothing).$$
(∅). (7)
We can define the analogue of the Gelfond-Lifschitz reduct of a CC -program, which we call the NSS-reduct of P, as follows. Let P¯ denote the set of all transformed clauses derived from P. Given a set of atoms M, we eliminate from P¯ those clauses where some upper-constraint (Xiui) is not satisfied by M, i.e.

|M ∩ Xi| > ui. In the remaining clauses, the constraints of the form Xiui are eliminated altogether. This leaves us with a CC -Horn program PM. We then define **CCGL**P (M) to be the least fixed point of TPM and say that M is a CC -stable model if M = **CCGL**P (M). The equivalence of this construction and the original construction in [SNS02] for normal CC -programs is shown in [MNT07].

Next we define the analogues of P-proof schemes for normal CC -programs, i.e.

programs which consists entirely of clauses of the form (4). This is done by induction as follows. When C = p ← X1u1**, . . . , X**kuk is a normal CC -clause without the cardinality-constraints of the form liXithen

$\eqref{eq:walpha}$. 
$u_k\}$). 

$$\tau_{1}u_{1},\ldots,X_{k}u_{k}\}.$$
$\star\quad\star\quad\star$
$ n\rangle,U\rangle$. 
hhC, pi, {X1u1**, . . . , X**kuk}i is a P-CC -proof scheme with support {X1u1**, . . . , X**kuk}. Likewise, when

$\mathbf{a}\cdot\mathbf{b}=\mathbf{a}\cdot\mathbf{b}\cdot\mathbf{c}$. 
$\overline{\phantom{\rule{1ex}{0ex}}}=\phantom{\rule{1ex}{0ex}}\backslash\backslash\backslash\phantom{\rule{1ex}{0ex}}\mathbb{C}$
S = hhC1, p1i, . . . ,hCn, pni, Ui is a P-CC -proof scheme,

$$p\gets l_{1}X_{1},\ldots,l_{m}X_{m},X_{1}u_{1},\ldots,X_{m}u_{m}$$
is a clause in $P$, and $|X_{1}\cap\{p_{1},\ldots,p_{n}\}|\geq l_{1},\ldots,|X_{m}\cap\{p_{1},\ldots,p_{n}\}|\geq l_{m}$, then  $$\langle\langle C_{1},p_{1}\rangle,\ldots,\langle C_{n},p_{n}\rangle,\langle C,p\rangle,U\cup\{X_{1}u_{1},\ldots,X_{m}u_{m}\}\rangle$$

is a P-CC -proof scheme with support U ∪ {X1u1**, . . . X**mum}. The notion of admittance of a P-CC -proof scheme is similar to the notion of admittance of P-proof scheme for normal programs P. That is, if S = hhC1, p1i, . . . ,hCn, pni,hC, pi, Ui is a CC -proof scheme with support U = {X1u1**, . . . X**nun}, then S is admitted by M if for every Xiui ∈ U, M |= Xiui, i.e. |M ∩ Xi| ≤ ui. Similarly, we can associate a propositional formula φU so that M admits S if and only if M |= φU as follows:

$$\phi_{U}=\bigwedge_{i=1}^{n}\bigvee_{W\subseteq X_{i},|W|=|X_{i}|-u_{i}}\neg W.$$
¬W. (8)
$$({\boldsymbol{8}})$$

$$15$$
