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/02 10:59] vkuncak |
sav08:definition_of_resolution_for_fol [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 2: | Line 2: | ||
This is the definition of resolution rule for first-order logic clauses. | This is the definition of resolution rule for first-order logic clauses. | ||
- | \[ | + | \begin{equation*} |
\frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} | \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} | ||
{subst(\sigma)(C' \cup D')} | {subst(\sigma)(C' \cup D')} | ||
- | \] | + | \end{equation*} |
where $\sigma_1$, $\sigma_2$ are renamings, $\sigma = mgu(\{subst(\sigma_1)(A_1),subst(\sigma_2)(A_2)\})$, | 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)$. | where $C' = subst(\sigma_1)(C)$ and $D' = subst(\sigma_2)(D)$. |