Can someone explain with a hands on example how the Gelfond Lifschitz reduct works in order to check stable model semantics?


a simple example here - at least as far as I understand the thing. So far grounding is clear to me - but the the application of the reduct is not. My goal in the end is to check stable model semantics of a program P and a supplied model M

Let i, j be constant symbols and X, Y be variables. Consider

d(X,Y,Z) :- a(X), b(Y), c(Z).
c(X) :- a(X), not b(X).

Decide using the Gelfond-Lifschitz reduct whether the interpretation I = {a(i), b(j), c(i), d(i, j, i)} is a stable model of P. Then the grounding looks like:

c(i):- a(i), not b(i).
c(j):- a(j), not b(j).
d(i,i,i) :- a(i), b(i), c(i).
d(i,i,j) :- a(i), b(i), c(j).
d(i,j,j) :- a(i), b(j), c(j).
d(j,j,j) :- a(j), b(j), c(j).
d(j,j,i) :- a(j), b(j), c(i).
d(j,i,i) :- a(j), b(i), c(i).
d(j,i,j) :- a(j), b(i), c(j).
d(i,j,i) :- a(i), b(j), c(i).

Now I start to apply the reduct. To me only the simple bits are clear:

P = {a(i), b(i), ... unclear part}

What is lacking & unclear to me: - removal of default negations - removal of not applicable formulas


Due to b(j)., c(j):- a(j), not b(j). is not applicable and needs to be removed. As all negated literals are deleted, c(i):- a(i), not b(i). is converted to c(i):- a(i).
Therefore, as I = {a(i), b(j), c(i), d(i, j, i)} is minimal representation of the remaining P, it is also stable.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.