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

Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein Widerlegungsverfahren: Statt direkt die Allgemeingültigkeit einer Formel zu zeigen, leitet es 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 ,  Klauseln einer aussagenlogischen Formel, die in konjunktiver Normalform vorliegt. Gibt es ein Literal , welches in  positiv und in  negativ vorkommt, ist die Vereinigung beider Klauseln ohne das positive und negative Literal  eine Resolvente (auch: der Resolvent) . Das heißt insbesondere: Gibt es kein komplementäres Literal, so gibt es auch keine Resolvente.

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

Anders notiert: Aus
 
wird auf die Resolvente
 
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  eine notwendige Bedingung für die Ausgangsklauseln  und  ist, gilt
 .
Man sagt  folgt aus  und . Hieraus folgt der Beweis zur Korrektheit der Resolution:

Res-Operator 

Das Ausführen eines einzelnen Resolutionsschrittes wird mit dem Res-Operator notiert:
, wobei  eine Resolvente zweier Klauseln aus  ist

Mit  bezeichnet man die Vereinigung aller möglichen Resolutionsschritte auf .

Somit sind folgende Aussagen möglich:
 ist die leere Klausel Element von , ist  unerfüllbar und
 ist die leere Klausel Element von , ist  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  und  bezeichnet
 die Quantoren  (der Existenzquantor) und  (der Allquantor),
 Konstanten, beispielsweise 
 ein- und mehrwertige Funktionen, üblicherweise mit Symbolen wie  oder  bezeichnet.

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

(Anmerkung: Setzen wir  und , so liefert uns die obige Formel die formal-logische Definition der Stetigkeit der Funktion  im Punkt .)

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.

 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.
 Durch die Anwendung von Skolemfunktionen eliminiert man alle Existenzquantoren  aus der Formel und bringt sie in die Skolemform.
 Nun sind alle Variablen in der Funktion an Allquantoren  gebunden. Trifft man die Übereinkunft, Konstanten und Variablen unterschiedlich zu bezeichnen, beispielsweise Konstanten mit  und Variablen mit , 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:

Substitution und Vereinheitlichung 

Die Formeln

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

Man erhält also die beiden Terme

die sich offensichtlich miteinander resolvieren lassen.

Folgende Ersetzungen sind möglich:

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:

Sei  eine Menge von Variablen. Sei  eine Menge von Termen, die aus Funktionen, Variablen oder Konstanten zusammengesetzt sein können.

 Ein System  von Ersetzungen  heißt eine Substitution.

Seien  Literale über demselben Prädikat , wobei die  wiederum Terme sind.

 Eine Substitution  heißt eine Vereinheitlichung (oder auch Unifikator) von , wenn durch die Anwendung von  die Argumente aller Literale zur Übereinstimmung gebracht werden, das heißt, wenn .

Zwei Literale über demselben Prädikat haben nicht notwendigerweise eine Vereinheitlichung. Beispielsweise lassen sich  und  nicht vereinheitlichen, wenn  und  unterschiedliche Konstanten sind.

 Eine Vereinheitlichung  von Literalen heißt allgemeinste Vereinheitlichung, wenn es für jede andere Vereinheitlichung  dieser Literale eine Substitution  gibt, so dass .

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  zwei Klauseln einer normalisierten prädikatenlogischen Aussage. Ohne Beschränkung der Allgemeinheit darf vorausgesetzt werden, dass diese keine übereinstimmenden Variablen enthalten (da sie durch einen Allquantor gebunden sind, können wir gleichnamige Variablen in einer Klausel umbenennen, auch wenn der Allquantor nicht mehr explizit geschrieben wird).
 Seien  und  positive bzw. negiert vorkommende Literale in  bzw. , die eine allgemeinste Vereinheitlichung  besitzen.
Dann heißt
  ein binärer Resolvent von  und .
 Sei ferner  eine Klausel mit einer Teilmenge von Literalen, die eine allgemeinste Vereinheitlichung  besitzt.

Dann heißt
  ein Faktor von .
Ein Resolvent zweier Klauseln  ist
 entweder ein binärer Resolvent von  und .
 oder ein binärer Resolvent von  und einem Faktor von .
 oder ein binärer Resolvent eines Faktors von  und .
 oder ein binärer Resolvent eines Faktors von  und eines Faktors von .
Das Resolutionsverfahren für prädikatenlogische Aussagen besteht darin, so lange solche Resolventen zu erzeugen, bis die leere Klausel erzeugt und damit der Widerspruchsbeweis erbracht ist.

Beispiel

Ein logisches Rätsel 

Wir wollen das Prinzip am Beispiel eines kleinen, nicht wörtlich zu nehmenden logischen Rätsels illustrieren:

Seit dem Altertum ist bekannt, dass alle Athener klug (1) und alle Spartaner heldenmütig (2) sind. Außerdem ist bekannt, dass ein profundes Misstrauen zwischen beiden Städten herrscht, so dass doppelte Stadtbürgerschaften ausgeschlossen sind (3). Unser nach Griechenland entsandter Forscher war neulich zu Gast bei einer Konferenz. Mit Ausnahme unseres Forschers stammte jeder der Anwesenden aus einer der beiden Städte (4).

Der Forscher kam ins Gespräch mit den Herren Diogenes, Platon und Euklid. Mit ihren berühmten Vorbildern hatten diese nur den Namen gemein. Die Herren zogen kräftig übereinander vom Leder. Euklid sagte: „Wenn Platon Spartaner ist, dann ist Diogenes feige!“ (5) – Platon behauptete: „Diogenes ist eine Memme, wenn Euklid Spartaner ist!“ (6) „Wenn Diogenes allerdings Athener ist, dann ist Euklid ein Waschlappen!“ (7) – Worauf sich Diogenes den Bart glatt strich und postulierte: „Wenn Platon Athener ist, dann ist Euklid ein Dummkopf!“ (8)

Bei aller Spitzzüngigkeit blieben die drei Herren mit ihren Behauptungen bei der Wahrheit. Wer kommt aus welcher Stadt?

Das Rätsel in Klauselform 

Wir setzen p für Platon, d für Diogenes, e für Euklid. Die Prädikate „ist Athener“, „ist Spartaner“, „ist heldenmütig“ und „ist klug“ bezeichnen wir mit A, S, H und K. Wir übersetzen die oben genannten Aussagen in die Klauselform und erhalten:

Die Auflösung 

Wir nehmen an, Platon sei Athener:

Nun wenden wir das Resolutionsprinzip an und erhalten:

Somit ist die Annahme (9) zum Widerspruch geführt. Sie ist mitsamt den aus ihr abgeleiteten Klauseln (10) bis (18) zu verwerfen. Wir erhalten stattdessen:

Nehmen wir nun an, Diogenes sei Spartaner, und wenden wir weiterhin das Resolutionsprinzip an:

Somit ist die Annahme (21) widerlegt und mitsamt den aus ihr abgeleiteten Klauseln (22) – (24) zu verwerfen. Wir erhalten stattdessen:

Nehmen wir an, Euklid sei Spartaner. Wir erhalten:

Also ist (27) falsch und samt (28) – (30) zu verwerfen. Wir erhalten stattdessen:

Platon ist Spartaner (20). Diogenes ist Athener (26), ebenso Euklid (32).

Terminierung und Komplexität 

Im Falle der Aussagenlogik terminiert das Verfahren: Es liefert in endlicher Zeit ein Ergebnis, ob eine vorgelegte Aussage erfüllbar ist. Die Rechenzeit wächst im allgemeinen Fall und mit den derzeit bekannten Verfahren exponentiell mit der Anzahl der Literale. Das Problem ist NP-vollständig.

Im Falle der Prädikatenlogik terminiert das Verfahren stets mit dem korrekten Ergebnis, wenn es auf eine unerfüllbare Formel angewendet wird. Bei einer erfüllbaren Formel kommt es jedoch vor, dass das Verfahren kein Ende findet. Man spricht von Semi-Entscheidbarkeit. 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.

Andere Kalküle im logischen Einsatz 

 Baumkalkül: in gewisser Weise unter den Kalkülen der nächste Verwandte des Resolutionskalküls
 axiomatische Kalküle
 Systeme natürlichen Schließens
 Sequenzenkalkül
 Existential Graphs

Quellen

Literatur 
 Chang, Chin-Liang; Lee, Richard Char-Tung: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973, ISBN 0-12-170350-9

Weblinks 
 Vorlesungsskript von Habel und Eschenbach, 2009, Fachbereich Informatik, Universität Hamburg, mit anschaulichen grafischen Darstellungen (PDF-Datei; 410 kB)
 Vorlesungsskript von Bernhard Beckert, 2006, Universität Koblenz-Landau (PDF-Datei; 197 kB)
 Logic for Computer Scientists, von Ulrich Furbach, Universität Koblenz-Landau

Mathematische Logik
Logikkalkül