Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:definition_of_resolution_for_fol [2008/04/01 18:19]
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 $C'$ is renaming of $C$, where $D'$ is renaming of $D$, and where $\sigma = mgu(\{C'​,D'\})$.+where $\sigma_1$, $\sigma_2are 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]].
  
 
sav08/definition_of_resolution_for_fol.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice