Conditions in disjunctive literals

[marklaw]

Hi,

I'm trying to understand a very small disjunctive program:

a : b; c.
a :- b.
b :- c.

My (probably incorrect) understanding was that this should have a single answer set ({a, b, c}), but clingo says it is unsatisfiable. I've looked through the guide and it links to a paper by Amelia Harrison, that I'm trying to get my head around. However, I just wanted to make absolutely sure that the clingo output is correct before I go any further, because the following very similar program is satisfiable:

a : b :- d.
d ; c.
a :- b.
b :- c.

Apologies if I'm being extremely naïve, but I'd have thought those two programs to be equivalent (other than the auxiliary atom d).

[marklaw]

Ah. I think I understand it now. I can't find a resource on reducts with conditional literals, but do they essentially get evaluated when the reduct is constructed? If so, I suppose the top program above w.r.t. X={a, b, c} would be:

a ; c.
a :- b.
b :- c.

Which has a model {a} that is a subset of X; hence, X is not an answer set.

Is that the right idea? Is there a paper on reducts for conditional literals, or are infinitary formulas the only way to understand them?

[rkaminsk]

We have not documented conditional literals in the head of rules in the AG paper. You can see the rule

a : b; c.

as a shortcut for

a; c :- b.  % (1)
c :- not b. % (2)

that is, the case whether the condition is true of false can be shifted to the body of a rule. All programs I have seen so far use atoms that evaluate to facts as conditions so one only needs (1) and can even simplify by dropping the condition altogether.

[marklaw]

Thanks for getting back to me. The paper I was referring to was actually https://www.aaai.org/ocs/index.php/KR/KR14/paper/viewFile/7966/7912 and not the abstract gringo paper. Conditionals in the head are briefly discussed in Section 3.4.

Thanks for the translation. Am I right in thinking that this is equivalent to interpreting conditionals when constructing the reduct? i.e., for each H:C, if the interpretation entails C, delete C; otherwise, delete H:C. It seems to be for this simple example, but I just wanted to double check that this generalises.

All programs I have seen so far use atoms that evaluate to facts as conditions so one only needs (1) and can even simplify by dropping the condition altogether.

Yes, I was working with a much larger program, but only sent a small propositional example to illustrate my main point of confusion.

Thanks again for your help.

Mark

[rkaminsk]

Thanks for getting back to me. The paper I was referring to was actually https://www.aaai.org/ocs/index.php/KR/KR14/paper/viewFile/7966/7912 and not the abstract gringo paper. Conditionals in the head are briefly discussed in Section 3.4.

Yes, this is what the translation in gringo is based on. It is (strongly) equivalent to the (easier to understand?) translation I gave above.

Thanks for the translation. Am I right in thinking that this is equivalent to interpreting conditionals when constructing the reduct? i.e., for each H:C, if the interpretation entails C, delete C; otherwise, delete H:C. It seems to be for this simple example, but I just wanted to double check that this generalises.

No, you cannot simply delete C if it is true in the candidate. Just have a look at the above translation. It introduces a positive occurrence in the rule body.

[marklaw]

Okay. Thanks for the clarification!