Resolutionslemma
Einfache Sprache
Def. Resolutionslemma
Sei $M$ eine Menge von Klauseln, $K,K'\in M$ und $X_i$ ein Aussagenlogische Variable so, dass $X_i\in K$ und $\neg X_i\in K'$, dann gilt
$$\left\{\bigvee K\mid K\in M\right\}\models\bigvee\mathrm{res}_{X_i}(K,K')\;.$$
Beweis: Sei $\beta$ eine erfüllende Belegung für alle Klauseln in $M$, also
$$\beta\models\left\{\bigvee K\mid K\in M\right\}\;.$$Dann gilt auch $\beta\models\bigvee K,\bigvee K'\;.$
Wir machen nun einen Fallunterscheidung über die Belegung von $\beta$ für $X_i$.
Fall 1: Sei $\beta(X_i) = 1$, dann gilt nach der Annahmen und $\beta\not\models\neg X_i$, dass $\beta\models\bigvee K'$. Also auch $\beta\models\bigvee\left(K'\setminus\{\neg X_i\}\right)$. Daraus folgt, dass
$$\beta\models\bigvee\left(K\setminus\{X_i\}\cup K'\setminus\{\neg X_i\}\right) = \bigvee\mathrm{res}_{X_i}(K,K')\;.$$Fall 2: Sei $\beta(X_i) = 0$, dann gilt nach der Annahmen und $\beta\not\models\neg X_i$, dass $\beta\models\bigvee K$. Also auch $\beta\models\bigvee\left(K\setminus\{ X_i\}\right)$. Daraus folgt, dass
$$\beta\models\bigvee\left(K\setminus\{X_i\}\cup K'\setminus\{\neg X_i\}\right) = \bigvee\mathrm{res}_{X_i}(K,K')\;.$$In beiden Fällen gilt also $\beta\models \bigvee\mathrm{res}_{X_i}(K,K')\;.$