
$$\cap U=\emptyset\},$$

Transition Systems for Model Generators - A Unifying Approach 27 set, it follows that s(B)∩M 6= /0. Consequently, s(B) contains a literal from M. We pick an arbitrary one and call it f(B). The clause

$$\supset=\neg a\lor\bigvee.$$

C = ¬a∨_{f(B) | B ∈ *Bodies*(Π
o,U) and B
pos ∩U = /0}, (7)
is a reason for ¬a to be in M¬a with respect to [F,Π].

First, by the choice of f(B), for every B ∈ *Bodies*(Πo,U) and B
pos ∩ U = /0, f(B) ∈ M.

Consequently,

M |= ¬_{f(B) | B ∈ *Bodies*(Π
o,U) and B
pos ∩U = /0}· (8)
Second, since f(B) ∈ B, the loop formula

$$(\bigwedge_{u\in U}\neg u)\vee\bigvee\{\}.$$
$${}^{28}\cap U=\emptyset\rbrace$$

¬u)∨_{B | B ∈ *Bodies*(Π,U) and B
pos ∩U = /0} (9)
entails C. By Lemma on Loop Formulas, it follows that Πoentails C. Consequently, F,Πo|= C.

For a list M of literals, by *consistent*(M) we denote the longest consistent prefix of M.

For example, consistent(abc¬bd) = abc. A clause C is conflicting on a list M of literals with respect to an SM(ASP) theory [F,Π] if *consistent*(M) |= ¬C and F,Πo|= C.

For a state M||Γ reachable from /0||/0 in SML(ASP)F,Π, by rM we denote a function that maps every non-decision literal in M to its reason to be in M (with respect to [F,Π]).

By RM we denote the set consisting of the clauses rM(l), for each non-decision literal l ∈ *consistent*(M).

A resolution derivation of a clause C from a sequence of clauses C1,...,Cm is a sequence C1,...,Cm,...,Cn, where C ≡ Cl for some l ≤ n, and each clause Ciin the sequence is either a clause from C1,...,Cm or is derived by applying the resolution rule to clauses Cj and Ck, where j,k < i (we call such clauses derived). We say that a clause C is derived by a resolution derivation from a sequence of clauses C1,...,Cm if there is a resolution derivation of a clause C from C1,...,Cm.

Lemma 12 Let [F,Π] be an SM(ASP) theory, M||Γ a state in the graph SM(ASP)F,Π such that M is inconsistent, and C1 a clause in RM. If clause C2 is conflicting on M with respect to [F,Π],
then every clause C derived from C1 and C2 is also a conflicting clause on M with respect to [F,Π].

Proof Let us assume that C is derived from C1 and C2 by resolving on some literal l ∈ C1. Then, C2 is of the form l∨C
′2
.

From the fact that C1 ∈ RM, it follows that F,Πo|= C1 and that C1 has the form c1 ∨C
′1
, where *consistent*(M) |= ¬C
′1
. Since C2 is conflicting, *consistent*(M) |= ¬C2 and F,Πo|= C2. By the consistency of *consistent*(M), there is no literal in C
′1 such that its complement occurs in C2. Therefore l = c1 and, consequently, C = C
′1 ∨C
′2
. It follows that consistent(M) |= ¬C. Moreover, since F,Πo|= C1 and F,Πo|= C2 and C results from C1 and C2 by resolution, F,Πo|= C.