# Thread: An Issue on default logic

1. ## An Issue on default logic

We have the following sentences which I translated them to FOL by using the language:

Att(x) for "x attended the ceremony"
Likes(x,y) for "x likes y"
Rel(x,y) for "x is a relative of y"
Ab(x) for "x is an abnormal relative"

(a) Only all the normal relatives attended the wedding ceremony.
a) ∀x Att(x) ------ > ¬ Ab(x)

(b) Everybody who attended the ceremony was either a relative of the groom or a relative of the bride.
b) ∀x∀y∀z Att(x) -------> Rel (X, groom) \/ Rel (x, bride)

(c) Groom’s relatives normally like the groom.
c) ∀x Rel (x, Groom) /\ ¬ Ab(x) ------ > Like (x,groom)

(d) Bride’s relatives normally like the bride.
d) ∀z Rel (z, Groom) ¬ Ab(z) ------ > Like (z,groom)

(e) Peter does not like bride.
e) ¬ Likes (Peter, bride)

I suppose my translation is correct.

Now the are three questions:

(1) How can I show, by using FOL rules, that Peter likes the groom or he did not attend the ceremony.

(2) Check if the claim, that Peter does not like groom, is entailed by the knowledge base under GCWA.

(3) Show, that if the sentence “All the relatives of the groom are abnormal” was added to the knowledge base, it would follow, under the GCWA, that Peter does not like the groom.

Any idea? Thanks

2. b) ∀x∀y∀z Att(x) -------> Rel (X, groom) \/ Rel (x, bride)
The quantifiers over y and z are unnecessary.
(a) Only all the normal relatives attended the wedding ceremony.
a) ∀x Att(x) ------ > ¬ Ab(x)
"Only all" is a pretty fancy way of saying. I would say, your translation corresponds to "Only the normal relatives attended", while ∀x ¬ Ab(x) ------ > Att(x) would mean "All the normal relatives attended". Therefore, probably it should be an equivalence. However, your direction is sufficient to prove that Peter likes the groom or he did not attend the ceremony.

(1) How can I show, by using FOL rules, that Peter likes the groom or he did not attend the ceremony.
What FOL rules do you have in mind? Can you prove informally that this conclusion follows?

I encountered Generalized Closed World Assumption in the context of logic programming, as in this survey by K.R. Apt et al. You, however, consider the database consisting not only of Horn clauses, general clauses (where negations can be in the body) or disjunctive clauses, but also clauses where the head is a negative literal. Also, I am not sure about whether to have Norm(x) or Ab(x) in the language. One of the definitions of GCWA refers to minimal Herbrand models, which consist of atoms only; choosing the complement as the base atom may change which models are minimal. What is your definition of GCWA?

It seems to me that the empty interpretation is a model of this set of clauses; therefore, it is the only minimal model. Thus, the fact that Peter does not like groom follows under GCWA. However, the question seems to imply that it does not follows since it says that another clause has to be added.

3. Thanks emakarov,

That is quite a new topic to me, so I write down whatever I know. That may sound so basic to you.

I think it is OK to show the conclusion informally, and also Ab(x) can be used in the language.

The question mainly focuses on Circumscription and entailment under GCWA.

CWA is based on NAF (Negation as failure) in which we derive ¬P from the failure to derive P. It is exactly like ordinary knowledge base except with respect to an augmented knowledge base that include all negative 'atomic' facts that are not explicitly ruled out by the knowledge base.

GCWA is a version of CWA, in which we can assume an atom P be false only of it is the case that whenever a disjunction of atoms including that atom (P) is entailed by the knowledge base, the smaller disjunction without the atom (P) is also entailed. In other words, we cannot assume that P is false, when there is an entailed disjunction of atoms including P exist that cannot be reduced to a smaller entailed disjunction not including P.

In circumscription we minimize the extension of a selected predicates. Here we assume some predicates to be as false as possible for every object except those for which they are known to be true. In fact, this is a way to talk about abnormal cases where the default should not apply.

What do you think now? Thanks

4. I am still not sure if you can prove informally that Peter likes the groom or he did not attend the ceremony. Everything else is quite a bit more complicated.

Also, I assume that your knowledge base can have implications with negated atoms as conclusions.

(2) Check if the claim, that Peter does not like groom, is entailed by the knowledge base under GCWA.
This can be shown if (a) has a biconditional: ∀x Att(x) <-> ¬Ab(x). Let's call the knowledge base P. Also, let's write p for Peter, g for the groom and b for the bride. Then from (1) we have P |- Likes(p,g) \/ ¬Att(p), so, P |- Likes(p,g) \/ Ab(p) from the right-to-left direction of (a). On the other hand, it is not the case that P |- Ab(p): it is easy to construct a counter-model where Peter is normal, attends the ceremony, is a relative of the groom and likes the groom. Therefore, P does not imply ¬Likes(p,g) under GCWA.

For (3), let P' be P together with ∀x. Rel(x,g) -> Ab(x). Then one can show that P' |- Ab(p).

Suppose that P' |- Likes(p,g) \/ D for some disjunction of ground atoms D; we need to show that P' |- D. Now, I only know how to show M |= P' implies M |= D for all Herbrand models M. If this were proved for all models M, then one could use the completeness theorem to show P' |- D. I am not totally sure if P' |- D can be concluded from my reasoning, but I think it is plausible.

So, suppose that M |= P' for some Herbrand model M. Then we can construct another model M' such that M' is a subset of M, M' |= P' and it is not the case that M' |= Likes(p,g). Since by assumption and soundness P' |= Likes(p,g) \/ D, we have M' |= D, and since M' is a subset of M and D is a disjunction of atoms, M |= D, as required.

Now, M' = M - {Likes(p,g)}. Since P' |- Ab(p), the atom Ab(p) is in M and M'. It is left to check that M' |= P'. The only formula is P' that could become false during the transition from M to M' is

∀x Rel(x,g) /\ ¬Ab(x) -> Likes(x,groom)

namely, its special case when x = p. But then M' |= ¬Ab(p), a contradiction, since Ab(p) is in M'.

5. Thanks emakarov,

Seems complicated to me, so I am gone read it few times to see what I get...

Thanks again.