Die Resolutionsmethode

Die Lektion über die Semantik der Aussagenlogik zeigte, dass Allgemeingültigkeit und Erfüllbarkeit mit der Wahrheitstafel entscheidbar sind, zu einem Aufwand, der sich mit jeder Variablen verdoppelt, und kündigte Methoden an, die nicht verlangen, sie zu durchlaufen. Die Lektion über semantische Folgerung und Äquivalenz führte jede Folgerung auf eine Unerfüllbarkeit zurück: $\Gamma \models \varphi$ genau dann, wenn $\Gamma \cup \{\neg\varphi\}$ unerfüllbar ist. Die Lektionen über die Normalformen und über ihren Algorithmus gaben jeder Formel eine konjunktive Form, deren Allgemeingültigkeit man auf einen Blick sieht, deren Erfüllbarkeit aber nicht. Wenn dem so ist, fehlt ein Verfahren, das die Unerfüllbarkeit einer Konjunktion von Klauseln entscheidet, indem es auf den Klauseln selbst operiert. Dieses Verfahren ist die Resolution, 1965 von John Alan Robinson auf der Grundlage von Ideen von Martin Davis und Hilary Putnam (1960) vorgeschlagen; sie ist der Kern der Programme, die heute die Erfüllbarkeit von Formeln mit Millionen von Variablen entscheiden. Anders als der Kalkül der Einheit über die Deduktion, dessen Beziehungen zur Semantik die Lektionen über Korrektheit und Vollständigkeit und über den Kompaktheitssatz untersuchen, leitet die Resolution keine Konklusionen ab: Sie widerlegt Mengen. Diese Lektion beweist, dass sie dies korrekt und vollständig tut.

Wie in den vorigen Lektionen bezeichnen $p$, $q$, $r$, $s$ und $t$ die Variablen $v_1$ bis $v_5$; der Buchstabe $v$ ohne Index, und ebenso $w$, bezeichnen Belegungen; und $V(\varphi)$ ist die Menge der Variablen von $\varphi$.

Klauseln und Klauselmengen

Man erinnere sich aus der Lektion über die Normalformen, dass ein Literal eine Variable oder die Negation einer Variablen ist und dass das Komplement eines Literals $\ell$, geschrieben $\ell^{*}$, das Literal derselben Variablen mit dem anderen Vorzeichen ist; zwei zueinander komplementäre Literale bilden ein komplementäres Paar. Nach dem Lemma über die Negation eines Literals gilt $v(\ell^{*}) = 1 - v(\ell)$ für jede Belegung $v$. Dort war eine Klausel eine Disjunktion von Literalen; hier ist es zweckmäßig, Reihenfolge und Wiederholungen, die den Wert nicht ändern, zu vergessen und sich an die Menge zu halten.

Eine Klausel ist eine endliche Menge von Literalen. Die Klausel ohne Literale heißt leere Klausel und wird $\Box$ geschrieben. Eine Belegung $v$ erfüllt eine Klausel $C$, geschrieben $v \models C$, wenn irgendein Literal von $C$ den Wert $1$ unter $v$ hat; andernfalls widerlegt $v$ sie. Eine Klausel aus einem einzigen Literal heißt Einheitsklausel. Die Variablen einer Klausel bilden die Menge $V(C)$; die einer Menge $S$ von Klauseln die Menge $V(S)$, die Vereinigung der vorigen. Eine Belegung erfüllt eine Menge $S$ von Klauseln, $v \models S$, wenn sie jede ihrer Klauseln erfüllt; $S$ ist erfüllbar, wenn irgendeine Belegung sie erfüllt, und andernfalls unerfüllbar. Ist schließlich $S$ eine Klauselmenge und $C$ eine Klausel, so bedeutet $S \models C$, dass jede Belegung, die $S$ erfüllt, auch $C$ erfüllt.

Zwei Grenzfälle folgen aus der Definition, und es lohnt sich, sie festzuhalten. Die leere Klausel hat keine Literale; daher hat keines ihrer Literale den Wert $1$, und keine Belegung erfüllt sie: $\Box$ ist unerfüllbar, und ebenso jede Menge, die sie enthält. Die leere Klauselmenge dagegen hat keine Klauseln, die zu erfüllen wären, und jede Belegung erfüllt sie. Man darf beide nicht verwechseln: $\{\Box\}$ ist unerfüllbar, und $\emptyset$ wird von allen Belegungen erfüllt.

Eine Klausel, die ein komplementäres Paar enthält, heißt tautologisch: Sie stellt keine Bedingung und kann aus jeder Menge entfernt werden, ohne deren Modelle zu ändern. Die Klauseln als Mengen zu schreiben ist keine Laune der Notation. Will man aus $(p \vee q)$ und $(p \vee \neg q)$ die Formel $p$ gewinnen, so liefert die Disjunktion $(p \vee p)$, die zu $p$ äquivalent, aber nicht dieselbe Formel ist; mit Mengen gilt $\{p\} \cup \{p\} = \{p\}$, und die Verschmelzung wiederholter Literale geschieht von selbst.