Resolution (Logik)

Grundidee und Bedeutung

Die Resolution, auch Resolutionskalkül genannt, ist ein formales Verfahren, mit dem die Gültigkeit logischer Formeln geprüft wird. Sie arbeitet als Widerlegungsverfahren: Um zu zeigen, dass eine Formel allgemeingültig ist, wird ihre Verneinung angenommen und daraus ein Widerspruch hergeleitet. Gelingt dies, kann die verneinte Formel nicht erfüllt werden, also ist die ursprüngliche Formel gültig.

Da die Herleitung nach festen formalen Regeln erfolgt, lässt sie sich algorithmisch und damit durch Computerprogramme ausführen. Die Resolution gehört deshalb zu den bekanntesten Techniken des maschinengestützten Beweisens.

Resolution in der Aussagenlogik

Eine aussagenlogische Formel wird in konjunktiver Normalform betrachtet, also als Konjunktion von Klauseln. Eine Klausel ist eine Disjunktion von Literalen; ein Literal ist eine Aussagevariable oder deren Negation.

Seien C₁ und C₂ zwei Klauseln. Kommt ein Literal L in C₁ positiv und in C₂ als komplementäres Literal L̄ negativ vor, entsteht eine Resolvente Cᵣ, indem beide Klauseln vereinigt und L sowie L̄ entfernt werden:

Cᵣ = (C₁ ∖ {L}) ∪ (C₂ ∖ {L̄}).

Gibt es kein komplementäres Literal, gibt es auch keine Resolvente. In einem Schritt darf immer nur genau ein Literalpaar aufgelöst werden. Je nach Ausgangsklauseln können deshalb verschiedene Resolventen möglich sein. Beispielsweise folgt aus

(A₁ ∨ A₂ ∨ … ∨ Aₙ) ∧ (B₁ ∨ B₂ ∨ … ∨ Bₘ ∨ ¬A₁)

die Resolvente

A₂ ∨ … ∨ Aₙ ∨ B₁ ∨ … ∨ Bₘ.

Die Resolvente ist nicht mit den beiden Ausgangsklauseln logisch äquivalent. Sie ist aber eine notwendige Bedingung für deren gemeinsame Erfüllbarkeit. Es gilt:

(C₁ ∧ C₂) → Cᵣ.

Damit folgt Cᵣ logisch aus C₁ und C₂. Die Korrektheit beruht darauf, dass die entsprechende Implikation durch logische Umformungen auf ¬A₁ ∨ A₁ und damit auf den Wahrheitswert 1 zurückgeführt werden kann.

Besonders wichtig ist die leere Klausel. Sie ist stets unerfüllbar. Kann sie durch Resolution hergeleitet werden, ist die gesamte zugrunde liegende Formel unerfüllbar.

Ein einzelner Resolutionsschritt wird mit dem Res-Operator notiert:

Res(F) = F ∪ {R},

wobei R eine Resolvente zweier Klauseln aus F ist. Die Menge aller durch beliebig viele Schritte erzeugbaren Klauseln heißt

Res★(F) = ⋃ₙ∈ℕ Resⁿ(F).

Ist die leere Klausel in Res★(F) enthalten, ist F unerfüllbar. Ist sie in Res★(¬F) enthalten, ist F eine Tautologie, also unter jeder Belegung wahr.

Übertragung auf die Prädikatenlogik

Die Prädikatenlogik erster Stufe berücksichtigt zusätzlich zu logischen Verknüpfungen Variablen wie x und y, die Quantoren ∃ und ∀, Konstanten wie 0, 1 und π sowie ein- und mehrstellige Funktionen wie f(x) und g(x,y). Um Resolution darauf anwenden zu können, muss die zu widerlegende Formel zunächst normalisiert werden.

Zuerst wird sie in Pränexform gebracht: Alle Quantoren stehen am Anfang, während der restliche Teil die Gestalt einer konjunktiven Normalform erhält. Danach werden durch Skolemfunktionen sämtliche Existenzquantoren ∃ entfernt; es entsteht die Skolemform. Die verbleibenden Variablen sind an Allquantoren ∀ gebunden. Werden Konstanten und Variablen eindeutig unterschiedlich bezeichnet, kann man die Allquantoren weglassen und erhält die Klauselform.

So wird die Formel

∀x ∃y ∀z K(g(a,z),y) → K(g(f(a),f(z)),x)

beispielsweise zur Klausel

¬K(g(a,z),s(x)) ∨ K(g(f(a),f(z)),x),

wobei s eine Skolemfunktion ist.

Substitution, Vereinheitlichung und prädikatenlogische Resolventen

In der Prädikatenlogik müssen Literale oft zunächst durch Ersetzungen passend gemacht werden. Da eine freie Variable implizit für alle möglichen Werte steht, lassen sich etwa P(x) und ¬P(a) durch die Ersetzung x → a in P(a) und ¬P(a) überführen und anschließend resolvieren.

Eine Variable kann unter anderem ersetzt werden:

• durch eine Konstante, etwa P(x) → P(a),
• durch eine andere Variable, etwa P(x) → P(y),
• durch eine Funktion einer Variablen, etwa P(x) → P(f(y)).

Die Ersetzung muss innerhalb eines Literals konsistent erfolgen. Aus P(x,f(x)) darf P(a,f(a)) entstehen, aber nicht P(a,f(x)).

Ein System von Ersetzungen {x₁ → t₁, x₂ → t₂, …, xₙ → tₙ} heißt Substitution. Die Terme tᵢ dürfen aus Funktionen, Variablen oder Konstanten aufgebaut sein. Eine Substitution S heißt Vereinheitlichung oder Unifikator mehrerer Literale über demselben Prädikat, wenn diese nach ihrer Anwendung übereinstimmen: S(L₁) = S(L₂) = … = S(Lₘ). Nicht jedes Paar ist vereinheitlichbar; P(a) und P(b) können etwa nicht vereinheitlicht werden, wenn a und b verschiedene Konstanten sind.

Eine Vereinheitlichung S heißt allgemeinste Vereinheitlichung, wenn für jede andere Vereinheitlichung T eine Substitution V existiert, sodass T = S ∘ V gilt. Besitzt eine Menge von Literalen überhaupt eine Vereinheitlichung, besitzt sie auch eine allgemeinste Vereinheitlichung, die algorithmisch ermittelt werden kann.

Für die Resolution seien C₁ und C₂ normalisierte prädikatenlogische Klauseln ohne gemeinsame Variablennamen. Dies lässt sich durch Umbenennen erreichen, weil die Variablen allquantifiziert sind. Enthalten C₁ und C₂ ein positives beziehungsweise negatives Literal L₁ und L₂ mit einer allgemeinsten Vereinheitlichung S, so heißt

Cᵣ = S(C₁ ∪ C₂) ∖ {S(L₁), ¬S(L₂)}

ein binärer Resolvent.

Besitzt eine Teilmenge der Literale einer Klausel C eine allgemeinste Vereinheitlichung S, heißt S(C) ein Faktor von C. Ein Resolvent zweier Klauseln kann unmittelbar aus beiden Klauseln, aus einer Klausel und einem Faktor der anderen oder aus Faktoren beider Klauseln gebildet werden. Das Verfahren erzeugt solche Resolventen so lange, bis die leere Klausel und damit der gesuchte Widerspruch entsteht.

Beispiel, Grenzen und verwandte Kalküle

Ein Beispiel fragt nach der Herkunft von Platon, Diogenes und Euklid. Es gelten folgende Aussagen: Alle Athener sind klug, alle Spartaner heldenmütig, niemand besitzt beide Stadtbürgerschaften, und jeder Anwesende außer dem Forscher stammt aus einer der beiden Städte. Zusätzlich sind mehrere wahre Aussagen der drei Personen gegeben. Mit A für „ist Athener“, S für „ist Spartaner“, H für „ist heldenmütig“ und K für „ist klug“ entstehen unter anderem die Klauseln ¬A(x) ∨ K(x), ¬S(x) ∨ H(x), ¬A(x) ∨ ¬S(x) und A(x) ∨ S(x).

Die Annahme A(p), Platon sei Athener, führt durch wiederholte Substitution und Resolution schließlich sowohl zu S(e) als auch zu ¬S(e) und damit zur leeren Klausel. Also ist Platon kein Athener; aus A(p) ∨ S(p) folgt S(p). Die Annahme, Diogenes sei Spartaner, führt ebenfalls zur leeren Klausel, sodass A(d) gilt. Entsprechend wird die Annahme S(e) widerlegt, woraus A(e) folgt. Das Ergebnis lautet: Platon ist Spartaner, Diogenes und Euklid sind Athener.

In der Aussagenlogik terminiert das Resolutionsverfahren: Es entscheidet in endlicher Zeit, ob eine Formel erfüllbar ist. Die Rechenzeit wächst im allgemeinen Fall bei den derzeit bekannten Verfahren exponentiell mit der Anzahl der Literale; das Problem ist NP-vollständig.

In der Prädikatenlogik liefert das Verfahren bei einer unerfüllbaren Formel stets nach endlicher Zeit das korrekte Ergebnis. Bei einer erfüllbaren Formel kann es dagegen unbegrenzt weiterlaufen. Dies heißt Semi-Entscheidbarkeit. Eine allgemeine Terminierung würde ein Entscheidungsverfahren für prädikatenlogische Formeln ergeben; ein solches ist unmöglich, weil das Gültigkeitsproblem der Prädikatenlogik nicht entscheidbar ist.

Andere in der Logik eingesetzte Kalküle sind der Baumkalkül, der dem Resolutionskalkül in gewisser Weise am nächsten steht, axiomatische Kalküle, Systeme natürlichen Schließens, der Sequenzenkalkül und Existential Graphs.