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.
Reducing the Search Space
More powerful rules.
But more choices at each step.
If we try to do the proof, how do we know what to instantiate with?
Resolution with instantiation \[ \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
{subst(\sigma,C \cup D)}
\] such that .
Note: such that is called a unifier for .
Factoring with instantiation \[ \frac{C \cup \{A_1, A_2\}}
{subst(\sigma,C \cup D)}
\] where .
Further step: do we need to consider all unifiers?
Most general unifier. To compute it we can use the standard Unification algorithm.