Resolution (Logik)

Die Resolution der ist ein Verfahren der formalen Logik, um eine logische Formel auf Gültigkeit zu testen.

Die Resolution ist ein Verfahren des Widerspruchsbeweises: Statt direkt die Allgemeingültigkeit einer Formel zu zeigen, leitet sie einen logischen Widerspruch aus deren Verneinung ab.

Diese Herleitung geschieht mittels eines Algorithmus auf rein formalem Weg und kann deshalb von einem Computerprogramm durchgeführt werden. Die Resolution ist eine der bekanntesten Techniken des Maschinengestützten Beweisens.

Das Resolutionsverfahren in der Aussagenlogik

Resolvente (auch: Resolvent)

Seien $C_{1}$, $C_{2}$ Klauseln einer aussagenlogischen Formel, die in konjunktiver Normalform vorliegt. Gibt es ein Literal $L$, welches in $C_{1}$ positiv und in $C_{2}$ negativ vorkommt, ist die Vereinigung beider Klauseln ohne das positive und negative Literal $L$ eine Resolvente (auch: der Resolvent)$C_{R}$.

$L\in C_{1}$

${\overline {L}}\in C_{2}$

$C_{R}=(C_{1}\cup C_{2})\setminus \{L,{\overline {L}}\}$

Es darf immer nur genau ein Literal resolviert werden. Je nach Ausgangsklauseln ist die Bildung verschiedener Resolventen möglich.

Anders notiert: Aus

$(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})$

wird auf die Resolvente

$A_{2}\vee \dots \vee A_{n}\vee B_{1}\vee \dots \vee B_{m}$

geschlossen.

Die Resolvente ist nicht äquivalent zu den Ausgangsklauseln. Die Bedeutung der Resolvente liegt vielmehr darin, dass die Ausgangsklauseln nur dann beide gleichzeitig erfüllbar sind, wenn auch die Resolvente erfüllbar ist (notwendige Bedingung). Gelingt es die leere Klausel zu resolvieren, die stets unerfüllbar ist, ist somit die Unerfüllbarkeit der gesamten Formel gezeigt.

Beweis

Da die Resolvente $C_{R}$ eine notwendige Bedingung für die Ausgangsklauseln $C_{1}$ und $C_{2}$ ist, gilt

$(C_{1}\wedge C_{2})\rightarrow C_{R}$.

Man sagt $C_{R}$ folgt aus $C_{1}$ und $C_{2}$. Hieraus kann man folgenden Beweis zur Korrektheit der Resolution ableiten:

$[(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\rightarrow (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})$

$\equiv \neg [(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})$

$\equiv (\neg A_{1}\wedge \neg A_{2}\wedge \dots \wedge \neg A_{n})\vee (\neg B_{1}\wedge \neg B_{2}\wedge \dots \wedge \neg B_{m}\wedge A_{1})\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (B_{1}\vee B_{2}\vee \dots \vee B_{m})$

$\equiv (\neg A_{1}\vee A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (A_{1}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})$

$\equiv \neg A_{1}\vee A_{1}$

$\equiv 1$

Res-Operator

Das Ausführen eines einzelnen Resolutionsschrittes wird mit dem Res-Operator notiert:

$Res(F)=F\cup \{R\}$, wobei $R$ eine Resolvente zweier Klauseln aus $F$ ist

Mit $Res^{\star }(F)$ bezeichnet man die unendliche Menge aller möglichen Resolutionsschritte auf $F$.

Somit sind folgende Aussagen möglich:

1. ist die leere Klausel Element von $Res^{\star }(F)$, ist $F$ unerfüllbar und
2. ist die leere Klausel Element von $Res^{\star }(\neg F)$, ist $F$ eine Tautologie

Resolution und Prädikatenlogik

Problemstellung

Für interessantere Problemstellungen ist das Instrumentarium der Aussagenlogik nicht ausreichend. Das Prinzip der Resolution sollte von der einfachen Aussagenlogik auf die Prädikatenlogik erster Stufe ausgeweitet werden können. Neben logischen Literalen sind dabei zu berücksichtigen:

• Variablen (beispielsweise Zahlenvariablen), üblicherweise mit Symbolen wie $x$ und $y$ bezeichnet
• die Quantoren $\bigvee _{x}$ (es existiert ein, für das gilt ...) und $\bigwedge _{y}$ (für alle y gilt ...),
• Konstanten, beispielsweise $0,1,\pi \,$
• ein- und mehrwertige Funktionen, üblicherweise mit Symbolen wie $f(x)$ oder $g(x,y)$ bezeichnet.

Ein durchaus typisches Beispiel für eine prädikatenlogische Aussage ist:

1)	$\bigwedge _{x}\bigvee _{y}\bigwedge _{z}K(g(a,z),y)\implies K(g(f(a),f(z)),x)$

(Anmerkung: Setzen wir $g(t,u)=\vert t-u\vert \,$ und $K(v,w)\equiv (v<w)\,$, so liefert uns die obige Formel die formal-logische Definition der Stetigkeit der Funktion $f\,$ im Punkt $a\,$.)

Damit auf solche Aussagen die Resolution angewendet werden kann, müssen sie umgeformt und das oben beschriebene Verfahren erweitert werden.

Normalisierung

Die ersten Schritte bestehen darin, die zu widerlegende Aussage in eine Form zu bringen, die der konjunktiven Normalform der Aussagenlogik ähnelt.

1. Man bringt die zu widerlegende Formel in die Pränexform. Nach dieser Umformung stehen die Quantoren alle am Anfang der Formel, und der Rest der Formel hat die Gestalt einer konjunktiven Normalform.
2. Durch die Anwendung von Skolemfunktionen eliminiert man alle Existenzquantoren $\bigvee$ aus der Formel und bringt sie in die Skolemform.
3. Nun sind alle Variablen in der Funktion an Allquantoren $\bigwedge$ gebunden. Trifft man die Übereinkunft, Konstanten und Variablen unterschiedlich zu bezeichnen, beispielsweise Konstanten mit $a,b,c,a_{1},a_{2},a_{3},...\,$ und Variablen mit $x,y,z,x_{1},x_{2},x_{3},...\,$, dann kann auch auf die explizite Notation des Allquantors verzichtet werden. Man lässt ihn ebenfalls weg und erhält die Klauselform der Aussage.
   
   

Beispielsweise lautet die Klauselform der Formel 1) aus dem vorigen Abschnitt:

2)	$\neg K(g(a,z),s(x))\vee K(g(f(a),f(z)),x)$

Substitution und Vereinheitlichung

Die Formeln

$P(x)\,$

und

$\neg P(a)\,$

scheinen auf den ersten Blick nicht resolvierbar zu sein, da sie sich in $x\,$ und $a\,$ unterscheiden. Da die freie Variable $x\,$ jedoch implizit ein Stellvertreter für alle $x\,$ ist, darf (unter anderem) $a\,$ für $x\,$ eingesetzt werden.

Man erhält also die beiden Terme

$P(a)\,$

und

$\neg P(a)\,$

die sich offensichtlich miteinander resolvieren lassen.

Folgende Ersetzungen sind möglich:

3a)	Ersetze Variable durch Konstante:	$P(x)\,$	$\rightarrow$	$P(a)\,$
3b)	Ersetze Variable durch eine andere Variable:	$P(x)\,$	$\rightarrow$	$P(y)\,$
3c)	Ersetze Variable durch Funktion einer Variablen:	$P(x)\,$	$\rightarrow$	$P(f(y))\,$

Die Ersetzung von Variablen in einem Literal muss in konsistenter Weise durchgeführt werden: Wird eine Variable an einer Stelle durch einen Term ersetzt, so muss dies innerhalb des Literals überall geschehen:

4a)	Korrekte Ersetzung:	$P(x,f(x))\,$	$\rightarrow$	$P(a,f(a))\,$
4b)	Verbotene Ersetzung:	$P(x,f(x))\,$	$\nrightarrow$	$P(a,f(x))\,$

Sei $\lbrace x_{1},x_{2},...,x_{n}\rbrace \,$ eine Menge von Variablen. Sei Sei $\lbrace t_{1},t_{2},...,t_{n}\rbrace \,$ eine Menge von Termen, die aus Funktionen, Variablen oder Konstanten zusammengesetzt sein können.

• Ein System $S\,$ von Ersetzungen $\lbrace x_{1}\rightarrow t_{1},x_{2}\rightarrow t_{2},...,x_{n}\rightarrow t_{n}\rbrace \,$ heißt eine Substitution.
  
  

Seien $L_{1}=P(t_{1},t_{2},...,t_{n}),L_{2}=P(u_{1},u_{2},...,u_{n}),...,L_{m}=P(v_{1},v_{2},...,v_{n})\,$ Literale über demselben Prädikat $P\,$, wobei die $t_{i},u_{i},...,v_{i}\,$ wiederum Terme sind.

• Eine Substitution $S\,$ heißt eine Vereinheitlichung von $L_{1},L_{2}...L_{m}\,$, wenn durch die Anwendung von $S\,$ die Argumente aller Literale zur Übereinstimmung gebracht werden, das heißt, wenn $S(L_{1})=S(L_{2})=...=S(L_{m})\,$.
  
  

Zwei Literale über demselben Prädikat haben nicht notwendigerweise eine Vereinheitlichung. Beispielsweise lassen sich $P(a)\,$ und $P(b)\,$ nicht vereinheitlichen, wenn $a\,$ und $b\,$ unterschiedliche Konstanten sind.

• Eine Vereinheitlichung $S\,$ von Literalen heißt allgemeinste Vereinheitlichung, wenn es für jede andere Vereinheitlichung dieser Literale eine Substitution $V\,$ gibt, so dass $T=S\circ V\,$.
  
  

Wenn eine Menge von Literalen eine Vereinheitlichung besitzt, dann besitzt sie eine allgemeinste Vereinheitlichung. Diese kann mit Hilfe eines relativ einfachen Algorithmus ermittelt werden.

Resolution prädikatenlogischer Klauseln

Mit diesem Instrumentarium kann das Resolutionsverfahren auf Aussagen der Prädikatenlogik ausgeweitet werden.

• Seien $C_{1},C_{2}\,$ zwei Klauseln einer normalisierten prädikatenlogischen Aussage. Ohne Beschränkung der Allgemeinheit darf vorausgesetzt werden, dass diese keine übereinstimmenden Variablen enthalten.
• Seien $L_{1}\,$ und $L_{2}\,$ positive bzw. negiert vorkommende Literale in $C_{1}\,$ bzw. $C_{2}\,$, die eine allgemeinste Vereinheitlichung $S\,$ besitzen.

Dann heißt

• $C_{R}=(C_{1}\cup C_{2})\setminus \{S(L_{1}),\neg S(L_{2})\}$ ein binärer Resolvent von $C_{1}\,$ und $C_{2}\,$.
  
  

• Sei ferner $C\,$ eine Klausel mit einer Teilmenge von Literalen, die eine allgemeinste Vereinheitlichung $S\,$ besitzt.

Dann heißt

• $S(C)\,$ ein Faktor von $C\,$.
  
  

Ein Resolvent zweier Klauseln $C_{1},C_{2}\,$ ist

• entweder ein binärer Resolvent von $C_{1}\,$ und $C_{2}\,$.
• oder ein binärer Resolvent von $C_{1}\,$ und eines Faktors von $C_{2}\,$.
• oder ein binärer Resolvent von eines Faktors von $C_{1}\,$ und $C_{2}\,$.
• oder ein binärer Resolvent eines Faktors von $C_{1}\,$ und eines Faktors von $C_{2}\,$.
  
  

Das Resolutionsverfahren für prädikatenlogische Aussagen besteht darin, so lange solche Resolventen zu erzeugen, bis die leere Klausel erzeugt und damit der Wirderspruchsbeweis erbracht ist.

Terminiertheit und Komplexität

Im Falle der Aussagenlogik terminiert das Verfahren: Es liefert stets in endlicher Zeit ein Ergebnis, ob eine vorgelegte Aussage wahr oder falsch ist. Es gehört allerdings zur Klasse der NP-vollständigen Verfahren, das heißt, dass im Allgemeinen die Rechenzeit exponentiell mit der Anzahl der Literale wächst.

Im Falle der Prädikatenlogik terminiert das Verfahren zwar stets mit dem korrekten Ergebnis, wenn ihm eine tautologische Formel vorgelegt wird. Im allgemeinen Fall kommt es jedoch vor, dass das Verfahren kein Ende findet. Wäre es anders, dann wäre das Resolutionsverfahren ein Algorithmus, um prädikatenlogische Formeln allgemein zu entscheiden - was unmöglich ist, da das Gültigkeitsproblem in der Prädikatenlogik nicht entscheidbar ist.

Literatur

Chang, Chin-Liang; Lee, Richard Char-Tung: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973, ISBN 0121703509

Weblinks

• Vorlesungsskript von Habel und Eschenbach, 2002, Fachbereich Informatik, Universität Hamburg, mit anschaulichen grafischen Darstellungen
• Vorlesungsskript von Bernhard Beckert, 2006, Universität Koblenz-Landau