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.