MN(S ∪ {¬aˆi}) = MOD(S **∪ {¬**aˆi}).

So (i) - (iii) imply MN(S1∪ {¬aˆi}) = MOD(S ∪ {¬aˆi})−MOD(S ∪ {¬aˆ1}) = MOD(S1**∪ {¬**aˆi}).

Hence ˆai **has the kernel property in** S1.

Step. Suppose kernel atoms ˆa1, . . . , aˆi (1 ≤ i < k**) have been included in**
S such that Si = S ∪ {aˆ1, . . . , aˆi}**. Then by the same argument as above** Siis consistent, and for all i < j ≤ k we have ˆaj ∈ tk(Si). Hence Sk = S ∪ tk(S**) is**
consistent.

So all kernel atoms of S can be included into S **in any order preserving**
consistency of the augmented set. However, this may not be true regarding a non-kernel typical atom ˆb of S such that ˆb 6∈ tk(S). Since b **does not possess** the kernel property, MN(S ∪ {¬ˆb}) ⊂ MOD(S ∪ {¬ˆb}**). So unlike the situation**
described by Lemma 4.1, inclusion into S of tk(S**) (or even of any literal** l consistent with S) may cancel all models of MOD(S ∪ {ˆb}**) and of** MN(S ∪
{¬ˆb}). Since the latter set is just a proper subset of MOD(S ∪ {¬ˆb}**), we get** MOD(S ∪ tk(S)) = MOD(S ∪ {¬ˆb}) − MN(S ∪ {¬ˆb}) 6= ∅. Hence ˆb **is false**
in all models of MOD(S ∪ tk(S)) and so inconsistent with S ∪ tk(S**) (or with**
S ∪ {l}**, respectively). Thus typical kernel is the largest set of atoms necessarily**
consistent with any S. ✷
The following algorithm checks for S **presented in a propositional CNF**
whether a typical atom ˆa **is its kernel atom.**
Algorithm 4.1 (Clauses c ∈ S are sets of literals; aˆ **is a typical atom of** S).

1. Count N1 = |MOD(S **∪ {¬**aˆ})|; 2. Compute S1 = {c − {¬aˆ} | c ∈ S ∧ aˆ 6∈ c};
3. Compute S2 = {c − {aˆ} | c ∈ S ∧ ¬aˆ 6∈ c}; 4. Count N2 = |MOD(S1 ∪ S2)|; 5. If N1 = N2 return "Yes, aˆ is a kernel atom of S**" else return "No".** ✷
There is a bijection between MOD(S1) and MOS(S ∪ {aˆ}**), and between**
MOD(S2) and MOD(S ∪ {¬aˆ}) such that to every model m′ ∈ MOD(S1)
corresponds a model (m′ ∪ {aˆ}) ∈ MOD(S ∪ {aˆ}**) and to every model**
m′′ ∈ MOD(S2) corresponds a model (m′′ ∪ {¬aˆ}) ∈ MOD(S ∪ {¬aˆ}**), and**
vice versa. Since MOD(S1 ∪ S2) = MOD(S1) ∩ MOD(S2**), to every model** m ∈ MOD(S1 ∪ S2) corresponds (m ∪ {aˆ}) ∈ MN(S ∪ {aˆ}) and (m **∪ {¬**aˆ}) ∈ MN(S∪{¬aˆ}), and vice versa. Hence, N2 = |MN(S∪{aˆ})| = |MN(S∪{¬aˆ})|.

So line 5 of the algorithm verifies whether ˆa **possesses the kernel property.**
Theorem 4.4 For all S, every typical model of S **includes** tk(S).

Proof. Suppose a typical model m of S does not include tk(S) as it contains a negation ¬aˆ of a kernel typical atom ˆa ∈ tk(S**). Due to the kernel**
property of ˆa, S has a model µ that is ˆa-neighbor of m **and hence contains ˆ**a.

So T(m) ⊂ T(µ). Hence, m **is not a typical model - a contradiction. By the**
same argument every typical model of S **includes** tk(S). ✷