LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:non-ground_instantiation_and_resolution [2008/04/01 17:45]
vkuncak
sav08:non-ground_instantiation_and_resolution [2008/04/02 10:50]
vkuncak
Line 31: Line 31:
 Illustration of rules. Illustration of rules.
  
-===== Reducing the Search Space =====+===== Combining Instantiation and Resolution ​=====
  
-More powerful rules.+These two are more powerful rules.
  
-But more choices at each step.+But we therefore have more choices at each step.
  
 If we try to do the proof, how do we know what to instantiate with? ++|we instantiate to enable subsequent resolution rule.++ If we try to do the proof, how do we know what to instantiate with? ++|we instantiate to enable subsequent resolution rule.++
Line 46: Line 46:
 such that $subst(\sigma_1)(A_1) = subst(\sigma_2)(A_2)$. such that $subst(\sigma_1)(A_1) = subst(\sigma_2)(A_2)$.
  
-This rule generalizes resolution and ground resolution.+This rule generalizes ​the above non-ground ​resolution and ground resolution.
  
 Note: if we apply instantiation that renames variables in each clause, then $\sigma_1$ and $\sigma_2$ can have disjoint domains and we let $\sigma = \sigma_1 \cup \sigma_2$, obtaining Note: if we apply instantiation that renames variables in each clause, then $\sigma_1$ and $\sigma_2$ can have disjoint domains and we let $\sigma = \sigma_1 \cup \sigma_2$, obtaining
Line 55: Line 55:
  
 Note: $\sigma$ such that $subst(\sigma)(A_1) = subst(\sigma)(A_2)$ is called a **unifier** for $\{A_1,​A_2\}$. Note: $\sigma$ such that $subst(\sigma)(A_1) = subst(\sigma)(A_2)$ is called a **unifier** for $\{A_1,​A_2\}$.
 +
 +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? Further step: do we need to consider all possible unifiers?
  
-Most general unifier for $\{A_1,​A_2\}$,​ denoted $mgu(A_1,​A_2)$+Most general unifier for $\{A_1,​A_2\}$,​ denoted $mgu(A_1,​A_2)$.
  
 To compute it we can use the standard [[Unification]] algorithm. To compute it we can use the standard [[Unification]] algorithm.