Stable Model Semantics

Stable models provide a declarative semantics for normal logic programs, particularly those in which negation is unstratified. When applied to extended logic programs, the same ideas produce "answer sets" instead. These terms are often used interchangeably. (Sergot)

Computing stable models is, in general, intractable (I think it's NP-complete). But a lot of the time you can get away with it, especially with modern SAT solvers.

If a program is stratified, then its unique stable, perfect, and iterated fixpoint models all coincide.
If a program is definite, then its unique stable, least Herbrand, perfect, and iterated fixpoint models all coincide.
That is, you don't lose anything on stratified or definite programs by using stable model semantics.

Where there are cyclic derivations, stable models and supported models don't necessarily agree. For tight programs, they do.

Marek Sergot's 491 Knowledge representation class at Imperial College covers stable models relatively cogently.
cf https://www.dbis.informatik.uni-goettingen.de/Teaching/DB/db-stable.pdf

Stable models

A stable model X of a normal logic program P is the least Herbrand model of P's reduct with respect to X. It can be shown that this also makes X a model of P.

Normal logic programs

"Normal" logic programs allow literals negated by failure ("naf-literals") in rule bodies.

Extended logic programs

"Extended" logic programs combine classical negation and negation by failure, allowing things like
p ← not ¬q
They subsume normal logic programs.

Immediate consequence operator (Tₚ) (defpgms-handout.pdf)

Given an interpretation I of a logic program P, Tₚ(I) is the set of literals that can be immediately deduced from I, that is, {L₀ ∈ P | L₀ ← L₁, …, Lₙ and L₀ ← L₁, …, Lₙ ∈ I}.

Models

A model of a normal logic program P is a set of atoms X with no immediate consequences, that is, Tₚ(X) ⊆ X. Alternatively, we could say X is a classical model of the clauses P¬ obtained by replacing every occurrence of not in P by ordinary, truth-functional negation ¬. (Sergot)

Reduct

A reduct of a logic program P wrt an interpretation I is a positive logic program obtained by:

  1. Deleting from P all rules containing any NAFed literal not entailed by I.
  2. Deleting from P's remaining rules all NAFed literals entailed by I.

https://dai.fmph.uniba.sk/~siska/asp/asp02.pdf is relatively clear