Prove using Resolution Refutation The following story is fro

Prove using Resolution Refutation:

The following story is from N. Wirth\'s (1976) Algorithms + data structures = programs. I married a widow (let\'s call her W) who has a grown-up daughter (call her D). My father (F), who visited us quite often, fell in love with my step-daughter and married her. Hence my father became my son-in-law and my step-daughter became my mother. Some months later, my wife gave birth to a son (S_1), who became the brother-in-law of my father, as well as my uncle. The wife of my father, that is, my step-daughter, also had a son (S_2) Using predicate calculus, create a set of expressions that represent the situation in the above story. Add expressions defining basic family relationships such as the definition of father-in-law and use modus ponens on this system to prove the conclusion that \"I am my own grandfather.\"

Solution

1.father (X,Y) ^ father (Y,Z) grandfather (X,Z)

2.father (X,Y) ^ married (Y,Z) father-in-law (X,Z)

3.father (X,Y) ^ mother (Y,Z) grandfather (X,Z)

4.father (X,Y) ^ father (X,Z) brother (Y,Z)

5.brother (X,Y) ^ grandfather (Z,Y) grandfather (Z,X)

6.married (I,W)

7.married (F,D)

8.father (I,S1)

9.father (I,D)

10.father (F,S2)

11.father (F,I)

12.mother (D,S2)

13.grandfather(I,S2)

USING 3:

9 ^ 12 grandfather (I, S2) (RESULT 1)

USING 4:

10 ^ 11 brother (S2,I) (RESULT 2)

USING 5: brother (X,Y) ^ grandfather (Z,Y) grandfather (Z,X)

Result2 ^ Result1

brother (I , S2) ^ grandfather (I, S2) grandfather (I, I)

THEREFORE, I AM MY OWN GRANDFATHER

%% prolog code

%% facts

male(i).
male(f).
male(s1).
male(s2).
married(i,w).
parent(w,d).
parent(f,i).
married(f,d).
parent(w,s1).
parent(i,s1).
parent(f,s2).
parent(d,s2).

%%rules

married(X,Y) :- tmarried(X,Y).
tmarried(X, Y) :- married(Y,X).

female(X) :- not(male(X)).

%% Normal relationships
father(Parent, Child) :-
    parent(Parent, Child),
    male(Parent).

mother(Parent, Child) :-
    parent(Parent, Child),
    female(Parent).

sibling(X,Y) :-
    parent(F, X),
    parent(F, Y), X = Y.

uncle(Uncle, Nephew) :-
    parent(Parent, Nephew),
    sibling(Parent, Uncle),
    male(Uncle).

grandparent(Grandfather, Grandchild) :-
    parent(X,Grandchild), parent(Grandfather,X).

%% In-law relationships
sibling_in_law(X,Y) :-
    parent(P,X),
    parent_in_law(P,Y),
    X = Y.

sibling_in_law(X,Y) :-
    parent(P,Y),
    parent_in_law(P,X),
    X = Y.

parent_in_law(Parent, Child) :-
    parent(Partner, Child),
    married(Parent, Partner).

uncle_in_law(Uncle, Nephew) :-
    parent_in_law(Parent, Nephew),
    sibling(Parent, Uncle),
    male(Uncle).

grandparent_in_law(Grandparent, Grandchild) :-
   ( parent_in_law(X, Grandchild), parent_in_law(Grandparent, X) );
   ( parent(X, Grandchild), parent_in_law(Grandparent, X) );
   ( parent_in_law(X, Grandchild), parent(Grandparent, X) ).

grandfather_in_law(Grandfather, Grandchild) :-
    grandparent_in_law(Grandfather, Grandchild),
    male(Grandfather).