# Homework Help: Skolemization and Knowledge base satisfaction

1. Jan 20, 2012

Greetings.

I'm studying for the exams and i'm having trouble with this one.

I have my KB: eq(a,b), eq(b,c), not eq(a,c)
And this is the Query: forall X, forall Y, forall Z ((eq(X,Y) and eq(Y,Z))=>eq(X,Z))

I want to proove that the KB doesn't satisfy the query. So, using the entailment procedure of this book (http://pt.scribd.com/doc/75920620/37...ment-Procedure [Broken]), i need to get the complement of the query. So...

~ forall X, forall Y, forall Z ((eq(X,Y) and eq(Y,Z))=>eq(X,Z))
exist X, exist Y, exist Z ~(~(eq(X,Y) and eq(Y,Z)) or (eq(X,Z)))
exist X, exist Y, exist Z (eq(X,Y) and eq(Y,Z) and ~eq(X,Z))

Now, i need to remove the existentials. So, in order to do that, i use skolemization. After replacing the variables with constants:

eq(o1,o2) and eq(o2,o3) and ~eq(o1,o3)

So, after all this, how do i proceed? I ask this because there are no variables to unify with...

Last edited by a moderator: May 5, 2017