Resolutionsbeweis

Einfache Sprache

Ein Resolutionsbeweis ergibt sich durch wiederholtes anwenden des Resolutionslemma

Def. Resolutionsbeweis

Ein Resolutionsbeweis einer Klausel $K$ aus einer Klauselmenge $M$ ist eine endliche Folge $K_0,K_1,\ldots,K_n = K$, die für alle $i\in[0,n]$ folgende Regeln erfüllen muss

• Voraussetzungsregel: $K_i\in M$.
• Resolutionsregel: Es existieren $j,k,l\in\mathbb N$ mit $jresolvierbar sein.
• Monotonieregel: Für alle $j\in[0,i-1]$ gilt $K_j\subseteq K_i$.

Wir sagen, dass sich $K$ aus $M$ per Resolution herleiten lässt.

Resolutionsbeweis

Sei $\Phi = \{\{X_0,X_1\}, \{\neg X_0,\neg X_1\}, \{X_1,X_2\}, \{\neg X_1,\neg X_2\}, \{X_0,X_2\}, \{\neg X_0,\neg X_2\}\}$. Wir zeigen, dass aus der Formelmenge $\Phi$ in Konjunktive Normalform falsch folgt.Also

$$\bigwedge\bigvee\Phi\models\bot\;.$$

Dazu machen folgenden Resolutionsbeweis:

| Step | Resolvente | Erläuterung | | —- | ———————– | ——————————— | | 1 | $\{X_0,X_1\}$ | Vorraussetzung | | 2 | $\{\neg X_1,\neg X_2\}$ | Vorraussetzung | | 3 | $\{X_0,\neg X_2\}$ | Resolution mit $X_1$ aus 1 und 2 | | 4 | $\{X_0,\neg X_2\}$ | Vorraussetzung | | 5 | $\{X_0\}$ | Resolution mit $X_2$ aus 3 und 4 | | 6 | $\{\neg X_0,\neg X_1\}$ | Vorraussetzung | | 7 | $\{ X_1, X_2\}$ | Vorraussetzung | | 8 | $\{\neg X_0, X_2\}$ | Resolution mit $X_1$ aus 6 und 7 | | 9 | $\{\neg X_0,\neg X_2\}$ | Vorraussetzung | | 10 | $\{\neg X_0\}$ | Resolution mit $X_2$ aus 8 und 9 | | 11 | $\emptyset$ | Resolution mit $X_0$ aus 5 und 10 |