I have a question on my assignment that I'm having a great deal of trouble with.(adsbygoogle = window.adsbygoogle || []).push({});

In this question we will

consider a simplified model of the “People you may know” application in Facebook. The

basic idea is that if two people have a common friend, then they may know each other. We

will also take into account the fact in Facebook the relation “friend” is symmetric, that is,

if X is a friend of Y , then Y is a friend of X.

Thus, as a problem description P, we have the following two predicate logic sentences:

8X8Y [(9Z(friend(X, Z) ^ friend(Z, Y ))) $ may know(X, Y )]

8X8Y [friend(X, Y ) ! friend(Y,X)]

Our goal is to show, using resolution refutation, that the following sentence g is implied by P:

8X8Y [may know(X, Y ) ! may know(Y,X)].

8 = universal quantifier

9 = existential quantifier

$ = biconditional

! = implication

I have been able to derive the following clauses (this is for a logical programming class):

c1: may_know(X,Y) :- friend(X,T), friend(T,Y)

c2: friend(X,f(X,Y,T)) :- may_know(X,Y)

c3: friend(f(X,Y,T),Y) :- may_know(X,Y)

c4: friend(Y,X) :- friend(X,Y)

c5: may_know(d,e) :-

c6: :- may_know(e,d)

I've attempted linear refutation which won't work. The question goes on to advise that you prove g from p "using your normal, mathematical, reasoning. Then, try to re-create the steps of your proof using resolution on your clauses." This is where I'm stuck, I'm not sure how I can prove g from p using either my clauses or my ordinary mathematical reasoning. Any help with this would be greatly appreciated.

**Physics Forums | Science Articles, Homework Help, Discussion**

Join Physics Forums Today!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# Homework Help: Predicate logic proof

**Physics Forums | Science Articles, Homework Help, Discussion**