Well-Founded Semantics and the Logic PC(ID). Let M be a set of (propositional) literals. By M we understand the set of the duals of the literals in M. A set U of atoms occurring in a program Π is unfounded on a consistent set M of literals with respect to Π if for every a ∈ U and every B ∈ *Bodies*(Π,a), M ∩s(B) 6= /0 or U ∩B
pos 6= /0. For every program Π and for every consistent set M of literals, the union of sets that are unfounded on M with respect to Π is also unfounded on M with respect to Π. Thus, under the assumptions above, there exists the greatest unfounded set on M with respect to Π. We denote this set by GUS(M,Π).

For every weakly normal program Π we define an operator WΠ on a set M of literals as follows

$$W_{\Pi}(M)=\left\{\begin{array}{ll}M\cup\{a\mid a\gets B\in\Pi\text{and}s(B)\subseteq M\}\cup\overline{G U S(M,\Pi)}&\text{if}M\text{is consistent}\\ At(\Pi)\cup\overline{At(\Pi)}&\text{otherwise.}\end{array}\right.$$

By W
fix Π
(M) we denote a fixpoint of the operator WΠ over a set M of literals. One can show that it always exists since WΠ is not only monotone but also increasing (for any set M of literals, M ⊆ WΠ(M)). The least fixpoint of WΠ, W
fix Π
(/0), is consistent and yields the wellfounded model of Π, which in general is three-valued. It is also written as lfp(WΠ). These definitions and properties were initially introduced for normal programs only (Van Gelder et al. 1991). They extend to programs in our syntax in a straightforward way, no changes in statements or arguments are needed (Lee 2005).

Let Π be a program and A a set of atoms. An atom a is open with respect to Π and A
if a ∈ A\ *Head*(Π). We denote the set of atoms that are open with respect to Π and A by O
Π A
. By ΠA we denote the logic program Π extended with the rules a ← *not not a* for each atom a ∈ O
Π A
. For instance, let Π be a program a ← b, not c b.(3)
Then, Π{c}is

$\vec{\epsilon}$ . 
c ← not not c a ← b, *not c* b.

We are ready to introduce the logic PC(ID) (Denecker 2000). A PC(ID) theory is a pair (F,Π), where F is a set of clauses and Π is a weakly normal logic program. For a PC(ID) theory (F,Π), by Πo we denote ΠAt(F∪Π) and by O
Π we denote O
Π
At(F∪Π)
(where At(F ∪ Π) stands for the set of atoms that occur in F and Π). Moreover, for a set M of literals and a set A of atoms, by MA we denote the set of those literals in M whose atoms occur in A. A set M of literals is complete over the set At of atoms if every atom in At occurs (possibly negated) in M and no other atoms occur in M.

Definition 1 Let (F,Π) be a PC(ID) theory. A consistent and complete (over At(F∪Π)) set M of literals is called a model of (F,Π) if
(i) M is a model of F, and
(ii) M = W
fix Πo (MO
Π).