Slide 14.12: An example of unification

An Example of Unification

Consider the greatest common divisor problem:

   gcd( u, 0, u ).
   gcd( u, v, w ) ← not zero( v ), gcd( v, u mod v, w ).

Now give the goal

   ← gcd( 15, 10, x ).

resolution fails using the first clause (10 does not match 0), so using the second clause and unifying gcd(u,v,w) with gcd(15,10,x) gives

   gcd( 15, 10, x ) ← not zero( 10 ),
             gcd( 10, 15 mode 10, x ), gcd( 15, 10, x ).

Since (i) not zero(10) is true, (ii) 15 mod 10 is 5, and (iii) cancel gcd(15,10,x) from both sides, we obtain the subgoal

   ← gcd( 10, 5, x ).

Note that this is just another goal to be resolved like the original goal. This we do by unification as before, obtaining

   gcd( 10, 5, x ) ← not zero( 5 ),
             gcd( 5, 10 mod 5, x ), gcd( 10, 5, x ).

and so get the further subgoal

   ← gcd( 5, 0, x ).

Now this matches the first rule

   gcd( u, 0, u ).

so instantiating x to 5 results in the empty statement, and the system will reply with something like

   Yes: x = 5