Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Homework Help: Skolemization and Knowledge base satisfaction

  1. Jan 20, 2012 #1
    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
  2. jcsd
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook

Can you offer guidance or do you also need help?
Draft saved Draft deleted