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:39]
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.++
  
-**Resolution with instantiation**+**Instantiation followed by resolution:**
 \[ \[
 \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
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)$.
  
-Resolution with instantiation ​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
  
 One complete proof system contains: One complete proof system contains:
 +  * instantiation followed by resolution
   * instantiation   * instantiation
-  * resolution with instantiation 
- 
-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: $\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\}$.
  
-Further step: do we need to consider all unifiers?+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 $\{A_1,​A_2\}$,​ denoted $mgu(A_1,​A_2)$.
  
-Most general unifier.  ​To compute it we can use the standard [[Unification]] algorithm.+To compute it we can use the standard [[Unification]] algorithm.