A marvellous example

We will study the domain of the family relationships. The system will deduce relations such as cousin based on basic relations, such as, parent and child.

We will define the following predicates :

	
   parent(X,Y)   -> X is parent of Y
   child(X,Y)    -> X is son of Y or X is daughter of Y
   brosis(X,Y) -> X is brother of Y, or X is sister of Y
   grandparent(X,Y)  -> X is grandparent of Y
   unaunt(X,Y)     -> X is uncle of Y or X is aunt of Y
   cousin(X,Y)   -> X is cousin of Y

Our axioms are :

    parent(X,Y)^parent(Y,Z)->grandparent(X,Z)
    child(Z,X)^parent(X,Y)->brosis(Y,Z)
    parent(X,Y)^brosis(X,Z)->unaunt(Z,Y)
    parent(X,Y)^brosis (X,Z) ^ parent (Z,T) -> cousin (Y,T)
    brosis(X,Y)->brosis(Y,X)

The Knowledge Base (KB) begins like this:

   >>list
    brosis(X,Y) -> brosis(Y,X)
    parent(X,Y) ^ brosis(X,Z) ^ parent(Z,T) -> cousin(Y,T)
    parent(X,Y) ^ brosis(X,Z) -> unaunt(Z,Y)
    child(Z,X) ^ parent(X,Y) -> brosis(Y,Z)
    parent(X,Y) ^ parent(Y,Z) -> grandparent(X,Z)

First, we introduce:

   >>save parent(juan,rocio)
    Number of new clausules in K.B.:1

   >>save parent(juan,jose)
    Number of new clausules in K.B.:1

   >>save parent(juan,pepe)
    Number of new clausules in K.B.:1

   >>save parent(maria,rocio)
    Number of new clausules in K.B.:1

   >>save parent(maria,jose)
    Number of new clausules in K.B.:1

   >>save parent(maria,pepe)
    Number of new clausules in K.B.:1

Listing the K.B. like this :

 >>list
    parent(maria,pepe)
    parent(maria,jose)
    parent(maria,rocio)
    parent(juan,pepe)
    parent(juan,jose)
    parent(juan,rocio)
    brosis(X,Y) -> brosis(Y,X)
    parent(X,Y) ^ brosis(X,Z) ^ parent(Z,T) -> cousin(Y,T)
    parent(X,Y) ^ brosis(X,Z) -> unaunt(Z,Y)
    child(Z,X) ^ parent(X,Y) -> brosis(Y,Z)
    parent(X,Y) ^ parent(Y,Z) -> grandparent(X,Z)

Now we introduce child(pepe,juan):

   >>save child(pepe,juan) 
    Number of new clausules in K.B.:6

   >>list
    brosis(pepe,pepe)
    brosis(pepe,jose)
    brosis(jose,pepe)
    brosis(pepe,rocio)
    brosis(rocio,pepe)
    child(pepe,juan)
    parent(maria,pepe)
    parent(maria,jose)
    parent(maria,rocio)
    parent(juan,pepe)
    parent(juan,jose)
    parent(juan,rocio)
    brosis(X,Y) -> brosis(Y,X)
    parent(X,Y) ^ brosis(X,Z) ^ parent(Z,T) -> cousin(Y,T)
    parent(X,Y) ^ brosis(X,Z) -> unaunt(Z,Y)
    child(Z,X) ^ parent(X,Y) -> brosis(Y,Z)
    parent(X,Y) ^ parent(Y,Z) -> grandparent(X,Z)

You can see that new relations appear. Notice the limitations of a system which does not handle equality.

The next relationship is parent(rocio,alberto):

   >>save parent(rocio,alberto)
    Number of new clausules in K.B.:4
 
   >>list
    unaunt(pepe,alberto)
    grandparent(maria,alberto)
    grandparent(juan,alberto)
    parent(rocio,alberto)
    brosis(pepe,pepe)
    brosis(pepe,jose)
    brosis(jose,pepe)
    brosis(pepe,rocio)
    brosis(rocio,pepe)
    child(pepe,juan)
    parent(maria,pepe)
    parent(maria,jose)
    parent(maria,rocio)
    parent(juan,pepe)
    parent(juan,jose)
    parent(juan,rocio)
    brosis(X,Y) -> brosis(Y,X)
    parent(X,Y) ^ brosis(X,Z) ^ parent(Z,T) -> cousin(Y,T)
    parent(X,Y) ^ brosis(X,Z) -> unaunt(Z,Y)
    child(Z,X) ^ parent(X,Y) -> brosis(Y,Z)
    parent(X,Y) ^ parent(Y,Z) -> grandparent(X,Z)

Finally:

   >>save brosis(jose,rocio)
    Number of new clausules in K.B.:3

   >>save parent(jose,david)
    Number of new clausules in K.B.:7

   >>list
    cousin(david,alberto)
    cousin(alberto,david)
    unaunt(rocio,david)
    unaunt(pepe,david)
    grandparent(maria,david)
    grandparent(juan,david)
    parent(jose,david)
    unaunt(jose,alberto)
    brosis(rocio,jose)
    brosis(jose,rocio)
    unaunt(pepe,alberto)
    grandparent(maria,alberto)
    grandparent(juan,alberto)
    parent(rocio,alberto)
    brosis(pepe,pepe)
    brosis(pepe,jose)
    brosis(jose,pepe)
    brosis(pepe,rocio)
    brosis(rocio,pepe)
    child(pepe,juan)
    parent(maria,pepe)
    parent(maria,jose)
    parent(maria,rocio)
    parent(juan,pepe)
    parent(juan,jose)
    parent(juan,rocio)
    brosis(X,Y) -> brosis(Y,X)
    parent(X,Y) ^ brosis(X,Z) ^ parent(Z,T) -> cousin(Y,T)
    parent(X,Y) ^ brosis(X,Z) -> unaunt(Z,Y)
    child(Z,X) ^ parent(X,Y) -> brosis(Y,Z)
    parent(X,Y) ^ parent(Y,Z) -> grandparent(X,Z)

The final K.B. is:

    cousin(david,alberto)
    cousin(alberto,david)
    unaunt(rocio,david)
    unaunt(pepe,david)
    unaunt(jose,alberto)
    unaunt(pepe,alberto)
    grandparent(maria,david)
    grandparent(juan,david)
    grandparent(maria,alberto)
    grandparent(juan,alberto)
    brosis(rocio,jose)
    brosis(pepe,pepe)
    brosis(pepe,jose)
    brosis(jose,pepe)
    brosis(pepe,rocio)
    brosis(rocio,pepe)

Now, in order to show how the backward-chaining mechanism works, and having the next KB:

   >>list
    parent(isa,david)
    brosis(isa,jose)
    parent(jose,antonio)
    parent(X,Y) ^ brosis(X,Z) ^ parent(Z,T) -> cousin(Y,T)
    parent(X,Y) ^ brosis(X,Z) -> unaunt(Z,Y)
    child(Z,X) ^ parent(X,Y) -> brosis(Y,Z)
    parent(X,Y) ^ parent(Y,Z) -> grandparent(X,Z)

Let's see, the command proof:

   >>proof cousin(david,antonio)
    { [ jose <- Z ],[ isa <- X ],[ david <- Y ],[ antonio <- T ] }

   >>proof unaunt(jose,david)
    { [ isa <- X ],[ jose <- Z ],[ david <- Y ] }

And finally, we exit from LFIAML:

   >>exit
    Goodbye!