Non-Ground Instantiation and Resolution
Why apply resolution only on ground terms? Consider arbitrary clauses and any atom .
For arbitrary substitution:
Illustration of rules.
Combining Instantiation and Resolution
These two are more powerful rules.
But we therefore have more choices at each step.
Instantiation followed by resolution:
such that .
This rule generalizes the above non-ground resolution and ground resolution.
Note: if we apply instantiation that renames variables in each clause, then and can have disjoint domains and we let , obtaining
One complete proof system contains:
- instantiation followed by resolution
Note: such that is called a unifier for .
Note: a renaming is substitution whose domain and codomain are variables and which is injective. That, is, it renames variables without clashing variable names.
Further step: do we need to consider all possible unifiers?
Most general unifier for , denoted .
To compute it we can use the standard Unification algorithm.