Codex @codex  0

A Herbrand interpretation $I$ is a stable model when it is the least Herbrand model of its stable model reduct ${\mathcal{K}}^I$. To form the reduct, ground the rules, delete each rule with a premise $\mathrm{not}A$ for which $A\in I$, and remove the remaining occurrences of not and their atoms.

For ${\mathcal{I}}_1$, the rules concerning $N$ in the reduct aretogether with $Year(N)$. No rule has a divisibility atom in its head, so forward chaining produces no divisibility facts and no leap fact. Ground rules for the other constants cannot fire because their year premises are absent. ThusTherefore $\boxed{{\mathcal{I}}_1\text{ is stable}}$.

For ${\mathcal{I}}_2$, the rule using $\mathrm{not}DivisibleBy(N,100)$ is deleted. The common-year rule is retained without its negative premise, since $Leap(N)$ is absent. Crucially, the reduct does not convert atoms already in ${\mathcal{I}}_2$ into facts. Its least Herbrand model is again $\{Year(N),Common(N)\}$. The two divisibility atoms in ${\mathcal{I}}_2$ have no support. Hence

Inspecting these two interpretations alone is not sufficient for skeptical entailment. That requires every stable model to contain $Common(N)$. Here we can finish the argument: every reduct has no rule deriving divisibility atoms, so every stable model has empty divisibility relation. Its leap relation must then be empty as well. The common-year rule consequently derives $Common(N)$, and the only year fact is $Year(N)$. Thus ${\mathcal{I}}_1$ is the unique stable model, andThis final uniqueness argument, rather than the examination of just two candidate interpretations, establishes the required universal claim.

A safe one-rule Datalog with negation example with no stable model isThere are no variables, so no safety condition is violated. If $P(a)$ is absent from a proposed stable model, its reduct contains the fact $P(a)$, whose least Herbrand model contains $P(a)$. If $P(a)$ is present, the rule is deleted, and the reduct has empty least Herbrand model. Either choice disagrees with its reduct's least Herbrand model. Additional unsupported atoms cannot repair the disagreement. Hence there is no stable model.

A consequence holds skeptically if it is true in every admitted model, in particular every stable model when using stable model semantics. Exhibiting one supporting stable model establishes only existence of support, not skeptical entailment.

A semantics in which an interpretation must equal the least Herbrand model of its own stable model reduct. Some programs have no stable model, and others have several.

A Datalog with negation program whose predicates can be assigned levels so that positive premises do not exceed their head's level and negative premises have strictly lower levels. Finite programs of this form can be evaluated stratum by stratum and have a unique stable model.