Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:definition_of_resolution_for_fol [2008/04/01 18:19] vkuncak |
sav08:definition_of_resolution_for_fol [2008/04/02 10:59] vkuncak |
||
|---|---|---|---|
| Line 6: | Line 6: | ||
| {subst(\sigma)(C' \cup D')} | {subst(\sigma)(C' \cup D')} | ||
| \] | \] | ||
| - | where $C'$ is renaming of $C$, where $D'$ is renaming of $D$, and where $\sigma = mgu(\{C',D'\})$. | + | where $\sigma_1$, $\sigma_2$ are renamings, $\sigma = mgu(\{subst(\sigma_1)(A_1),subst(\sigma_2)(A_2)\})$, |
| + | where $C' = subst(\sigma_1)(C)$ and $D' = subst(\sigma_2)(D)$. | ||
| We will call the above rule //mgu-resolution// if we need to differentiate it from [[Non-Ground Instantiation and Resolution|instantiation followed by resolution]]. | We will call the above rule //mgu-resolution// if we need to differentiate it from [[Non-Ground Instantiation and Resolution|instantiation followed by resolution]]. | ||