The quantifiers over y and z are unnecessary.b) ∀x∀y∀z Att(x) -------> Rel (X, groom) \/ Rel (x, bride)
"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.(a) Only all the normal relatives attended the wedding ceremony.
a) ∀x Att(x) ------ > ¬ Ab(x)
What FOL rules do you have in mind? Can you prove informally that this conclusion follows?(1) How can I show, by using FOL rules, that Peter likes the groom or he did not attend the ceremony.
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.