Solving Predicate Logic Proof Problem with Resolution Refutation

[houndstooth]

I have a question on my assignment that I'm having a great deal of trouble with.

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.

 

[grief]

If X may know Y, then by the first statement, there exists a Z such that X is a friend of Z and Z is a friend of Y. This means, by application of the second statement, that Y is a friend of Z and Z is a friend of X. So by the first statement, Y may know X

 

[piercas]

I understand your struggle with this problem as it involves complex concepts such as predicate logic and resolution refutation. However, it is important to approach this problem with a clear and logical mindset in order to find a solution.

Firstly, let's break down the problem into simpler parts. The given problem description states that if two people have a common friend, then they may know each other. We can represent this in predicate logic as 8X8Y [(9Z(friend(X, Z) ^ friend(Z, Y ))) $ may know(X, Y )]. This can be read as "For all X and Y, if there exists a Z such that X and Z are friends and Z and Y are friends, then X and Y may know each other."

The next sentence in the problem description states that the relation "friend" is symmetric, meaning that if X is a friend of Y, then Y is a friend of X. This can be represented as 8X8Y [friend(X, Y ) ! friend(Y,X)]. This can be read as "For all X and Y, if X is a friend of Y, then Y is a friend of X."

Now, our goal is to show that 8X8Y [may know(X, Y ) ! may know(Y,X)] is implied by the given sentences. This can be read as "For all X and Y, if X and Y may know each other, then Y and X may know each other."

To prove this using resolution refutation, we need to first convert the given sentences into conjunctive normal form (CNF). This involves breaking down the sentences into a series of clauses. The clauses that you have derived are a good starting point, but we need to make a few modifications in order to reach our goal.

Let's start with clause c1: may_know(X,Y) :- friend(X,T), friend(T,Y). This clause represents the first part of the problem description - if two people have a common friend, then they may know each other. However, we need to modify this clause in order to include the second part of the problem description - the symmetric nature of the "friend" relation. We can do this by adding another clause: may_know(X,Y) :- friend(Y,T), friend(T,X). This clause represents the idea that if Y is a friend of T and T is a friend of X, then X and Y