Slide 14.11: Unification

Slide 14.10: Examples of resolution
Slide 14.12: An example of unification
Home

Unification

The previous example demonstrates an additional requirement when we apply resolution to derive goals: To match statements that contain variables, we must set the variables equal to terms so that the statements become identical and can be canceled from both sides:

legs(x,4) ← mammal(x), arms(x,0), legs(horse,4).

⇓  x = horse

legs(horse,4)←mammal(horse),arms(horse,0),legs(horse,4).

This process of making statements identical is called unification, and variables that are set equal to patterns are said to be instantiated.

Unification is a binary operation whose purpose is to attempt to make its two operands the same.

Other than resolution and unification, the execution orders need to be considered too. For example, given the Horn clauses

   ancestor( x, y ) ← parent( x, z ), ancestor( z, y ).
   ancestor( x, x ).
   parent( amy, bob ).

if we provide the query

   ← ancestor( x, bob ).

there are two possible answers for this query:

If the assertion ancestor(x,x) is used, the solution is x=bob.

If the clause ancestor(x,y)←parent(x,z),ancestor(z,y) is used, the solution x=amy will be found.

A logic language must adopt a specific execution order to find the answers or no answer at all.