This is an old revision of the document!
Non-Ground Instantiation and Resolution
Non-Ground Resolution
Why apply resolution only on ground terms? Consider arbitrary clauses and any atom . \[ \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}}
{C \cup D}
\]
Non-Ground Instantiation
For arbitrary substitution: \[ \frac{C}{subst(\sigma)(C)} \]
Is this non-ground instantiation rule sound?
Illustration of rules.
Combining Instantiation and Resolution
These two are more powerful rules.
But we therefore have more choices at each step.
If we try to do the proof, how do we know what to instantiate with?
Instantiation followed by resolution: \[ \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
{subst(\sigma_1)(C) \cup subst(\sigma_2)(D)}
\] 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
- instantiation
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.