First Order Logic Unification

2
votes

I have a question about an exercise of FOL in which I have to prove if is it possible to unify two sentences and , in positive case , to show how to unify them.

1) f(g(a,X),g(Y,Y))=f(g(a,b),g(f(a),f(Z)))

2) f(cons(cons(a,b)))=f(cons(cons(a,nil))

For the first one I understood the procedure so I gave the value f(a) to Z and then I used the substitution o = {Y/f(a)} to obtain two identical sentences.

For the second one really I did not understand what is the semantic of the sentence and how can I unify it.

1
logicartificial-intelligencefirst-order-logic

1 Answers

1
votes

The unification algorithm is simple

  1. if both sides are constants (numbers, strings, atoms, etc.) the result unifies it it is the same one
  2. if one side is a variable, we add the subtitution of this variable by the other side
  3. if both sides are functions, it unifies if this is the same function (same name) and same parity (number of parameters), then unify recursively parameters.

With your examples:

  • f(g(a,X),g(Y,Y)) = f(g(a,b),g(f(a),f(Z))) 3rd case, same function (f) and same arity (2). So you have to unify parameters:

    • g(a,X) = g(a,b)
    • g(Y,Y) = G(f(a), f(Z))

g(a,X) unifies with g(a,b) because this is the same function (g) same arity (2). a = a unifies (case 1), X = b unifies (case 2) with substitution {X/b}

G(Y,Y) unifies with G(f(a), f(Z)) because this is the same function (g) same arity (2). then Y=f(a) => substitution {Y/f(a)} and Y=f(Z) => f(a) unifies with F(Z) {Z/a}

In the end you get o = {X/b, Y/f(a), Z/a}

  • f(cons(cons(a,b))) = f(cons(cons(a,nil)))

The same applies here. Same function (f) same arity (1). Unify cons(cons(a,b)) = cons(cons(a,nil)) Same function (cons) same arity (1). Unify cons(a,b) = cons(a,nil) Same function (cons), same arity (2). Unify a=a (OK), b=nil => NO

This does not unify.