Question

Read the following paragraph and answer the questions.

Every man does not hit a woman whom he loves. John and Bill are men and Mary is a woman. Mary loves either John or Bill. Bill hit Mary. Does Mary love John?

a) Represent the above sentences into FOL (First Order Logic) formulas with defining your ontology. (5 Points)

b) In order to get the correct answer, if you need additional knowledge give the additional FOL formulas. And write the question (answer) into FOL formula (3 Points).

c) Prove the answer is true by the refutation-resolution.

Answer 1

Solution:

a) Every man does not hit a woman whom he loves.

∀x (man(x)→∃y[(woman(y)∧~hit(x,y))→loves(x,y)])

John and Bill are men and Mary is a woman

Man(John)^Man(Bill)^Woman(Mary)

Mary loves either John or Bill (it is clear that not both) that means exclusive or. The logic expression for exclusive or is p⊕q=(p∧¬q)∨(¬p∧q)=(¬p∨¬q)∧(p∨q)=p<->q=p->q^q->p

[loves(Mary,John) -> loves(Mary,Bill)]^[loves(Mary,Bill) -> loves(Mary,John)]

Bill hit Mary.

hit(Bill,Mary)

b) Now, let us represent the Conjucative Normal Form for the first order logic given in part a).

1. ∀x (man(x)→∃y[(woman(y)∧~hit(x,y))→loves(x,y)])^

2. Man(John)^

3. Man(Bill)^

4. Woman(Mary)^

5. [loves(Mary,John) -> loves(Mary,Bill)]^[loves(Mary,Bill) -> loves(Mary,John)]^

6. hit(Bill,Mary)

Take the statement (1). Here y is Mary as she is woman and remove ∃ using existential elimination . x belongs to {John,Bill}

We know that p->q=~pvq.

Let p be man(x) and q be [(woman(y)∧~hit(x,y))→loves(x,y)]

So, we can write first statement as ~ ∀x (man(x)v[(woman(Mary)∧~hit(x,y))→loves(x,y)])

Now let us consider p as woman(Mary)∧~hit(x,y) and q as loves(x,y).

So, we can write the statement as ~[woman(Mary)∧~hit(x,y)]vloves(x,y)

~woman(Mary)vhit(x,y)vloves(x,y)

Statement 5 can be written as [~loves(Mary,John) v loves(Mary,Bill)] ^ [~ loves(Mary,Bill) v loves(Mary,John) ]

Finally, we can rewrite the sentences as

1. ~ ∀x man(x) v ~woman(Mary) v hit(x,Mary) v loves(x,Mary)^

2. Man(John)^

3. Man(Bill)^

4. Woman(Mary)^

5. [~loves(Mary,John) v loves(Mary,Bill)] ^

6. [~ loves(Mary,Bill) v loves(Mary,John) ] ^

7. hit(Bill,Mary)

Goal: love(Mary,John)

c) Refutation resolution: It is a technique to reach the goal by going with contradiction.

7.Take statement 1 and 2: We get ~woman(Mary) v hit(x,Mary) v loves(x,Mary) where x ={John}

8. Take statement 7 and 4: We get hit(John,Mary) v loves(John,Mary)

9. In the above statement we get two contradiction i.e...there is no statement hit(Jobn,Mary).

Hence we have Mary loves John.