Slide 14.9: Resolution (cont.)
Slide 14.11: Unification
Home

An Example of Resolution

A query is exactly the “opposite” of a fact—a Horn clause with no head: 
   mammal(horse) ←. or mammal(horse).     ——a fact
   ← mammal(horse).                       ——a query or goal
A slightly more complicated example is the following. Given the rules 
   legs( x, 2 ) ← mammal( x ), arms( x, 2 ).
   legs( x, 4 ) ← mammal( x ), arms( x, 0 ).
   mammal( horse ).
   arms( horse, 0 ).
If we supply the query 
   ← legs( horse, 4 ).
then applying resolution using the second rule, we get 
   legs(x,4) ← mammal(x), arms(x,0), legs(horse,4).
Now, to cancel the statements involving the predicate legs from each side, we have to match the variables x to horse, so we replace x by horse: 
   legs(horse,4)←mammal(horse),arms(horse,0),legs(horse,4).
and cancel to get the subgoals 
   ← mammal( horse ), arms( horse, 0 ).
Now we apply resolution twice more using the facts mammal(horse) and arms(horse,0) and cancel: 
   mammal( horse )  ← mammal( horse ), arms( horse, 0 ).
                    ← arms( horse, 0 ).
   arms( horse, 0 ) ← arms( horse, 0 ).
                    ←.
Since we have arrived at the empty statement, our original query is true.