Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:definition_of_resolution_for_fol [2008/04/01 18:11] vkuncak created |
sav08:definition_of_resolution_for_fol [2008/04/01 18:19] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Definition of Resolution for First-Order Logic ====== | ====== Definition of Resolution for First-Order Logic ====== | ||
+ | This is the definition of resolution rule for first-order logic clauses. | ||
\[ | \[ | ||
\frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} | \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} | ||
Line 6: | Line 7: | ||
\] | \] | ||
where $C'$ is renaming of $C$, where $D'$ is renaming of $D$, and where $\sigma = mgu(\{C',D'\})$. | where $C'$ is renaming of $C$, where $D'$ is renaming of $D$, and where $\sigma = mgu(\{C',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]]. | ||