Resolutionskalkül

Resolutionskalkül

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

Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein : Statt direkt die einer Formel zu zeigen, leitet es einen logischen Widerspruch aus deren Verneinung ab.

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

Inhaltsverzeichnis

Das Resolutionsverfahren in der Aussagenlogik

Resolvente (auch: Resolvent)

Seien C1, C2 einer Formel, die in vorliegt. Gibt es ein L, welches in C1 positiv und in C2 negativ vorkommt, ist die Vereinigung beider Klauseln ohne das positive und negative Literal L eine Resolvente (auch: der Resolvent)CR. Das heißt insbesondere: Gibt es kein komplementäres Literal, so gibt es auch keine Resolvente (C_R = \emptyset).

L \in C_1
\overline{L} \in C_2

C_R = (C_1 \setminus\{L\}) \cup (C_2 \setminus \{\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 (). 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 CR eine für die Ausgangsklauseln C1 und C2 ist, gilt

 (C_1 \wedge C_2) \rightarrow C_R .

Man sagt CR folgt aus C1 und C2. Hieraus folgt der Beweis zur Korrektheit der Resolution:

 [(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) = \bigcup_{n \in \mathbb{N}} Res^n(F) bezeichnet man die Vereinigung 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

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 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 x, für das gilt ...) und \bigwedge_y (für alle y gilt ...),
  • Konstanten, beispielsweise 0, 1, \pi \,
  • ein- und mehrwertige , ü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 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 . 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 .
  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 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 \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 (oder auch Unifikator) 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. 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 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 auch dann 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:

¬A(x) v K(x) (1)
¬S(x) v H(x) (2)
¬A(x) v ¬S(x) (3)
A(x) v S(x) (4)
¬S(p) v ¬H(d) (5)
¬S(e) v ¬H(d) (6)
¬A(d) v ¬H(e) (7)
¬A(p) v ¬K(e) (8)

Die Auflösung

Wir nehmen an, Platon sei Athener:

A(p) {Annahme} (9)

Nun wenden wir das Resolutionsprinzip an und erhalten:

¬K(e) {aus Resolution von (9) mit (8)} (10)
¬A(e) {aus Substitution von e für x und Resolution (10,1)} (11)
S(e) {Subs. (e:x), Res. (11,4)} (12)
¬H(d) {Res. (12,6)} (13)
¬S(d) {Subs. (d:x), Res. (13,2)} (14)
A(d) {Subs. (d:x), Res. (14,4)} (15)
¬H(e) {Res. (15,7)} (16)
¬S(e) {Subs. (e:x), Res. (16,2)} (17)
leere Klausel {Res. (17,12)} (18)

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:

¬A(p) {da (9) falsch ist} (19)
S(p) {Subs. (p:x), Res. (19,4)} (20)

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

S(d) {Annahme} (21)
H(d) {Subs. (d:x), Res. (21,2)} (22)
¬S(p) {Res. (22,5)} (23)
leere Klausel {Res. (23,20)} (24)

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

¬S(d) {da (21) falsch ist} (25)
A(d) {Subs. (d:x), Res. (25,4)} (26)

Nehmen wir an, Euklid sei Spartaner. Wir erhalten:

S(e) {Annahme} (27)
H(e) {Subs. (e:x), Res. (27, 2)} (28)
¬A(d) {Res. (28, 7)} (29)
leere Klausel {Res. (29,26)} (30)

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

¬S(e) {da (27) falsch ist} (31)
A(e) {Subs. (e:x), Res. (31,4)} (32)

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

Terminierung und Komplexität

Im Falle der Aussagenlogik 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, da es sich um ein Problem handelt.

Im Falle der Prädikatenlogik terminiert das Verfahren zwar stets mit dem korrekten Ergebnis, wenn ihm eine unerfüllbare Formel vorgelegt wird. Im allgemeinen Fall, bei einer erfüllbaren Formel, kommt es jedoch vor, dass das Verfahren kein Ende findet. Mit jedem Resolutionsschritt entstehen neue Klauseln, aber nicht die leere Klausel, die für den zu zeigenden Widerspruch steht. Man spricht also von . 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 ist.

Andere Kalküle im logischen Einsatz

  • : in gewisser Weise unter den Kalkülen der nächste Verwandte des Resolutionskalküls

Quellen

  1. Davis, Martin: Eliminating the Irrelevant from Mechanical Proofs. in: Journal of Symbolic Logic, ISSN 0022-4812, Vol. 32, No. 1 (Mar., 1967), pp. 118-119
  2. Chang, Chin-Liang; Lee, Richard Char-Tung: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973, ISBN 0-12-170350-9, S. 77ff
  3. Chang, Chin-Liang; Lee, Richard Char-Tung: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973, ISBN 0-12-170350-9, S. 80-81
  4. Haken, A. "The Intractability of Resolution", Theoretical Computer Science 39 (1985), pp. 297-308.

Literatur

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

Weblinks


Wikimedia Foundation.

Игры ⚽ Нужно решить контрольную?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Aussagenkalkül — Ein Aussagenkalkül ist ein Kalkül für die Aussagenlogik. Er leitet aus einer gegebenen Menge von Aussagen neue Aussagen her, die aus den gegebenen Aussagen aussagenlogisch folgen. Allgemein werden die Aussagen, aus denen hergeleitet wird,… …   Deutsch Wikipedia

  • Aussagenlogik — Die Aussagenlogik ist ein Teilgebiet der Logik, das sich mit Aussagen und deren Verknüpfung durch Junktoren befasst, ausgehend von strukturlosen Elementaraussagen (Atomen), denen ein Wahrheitswert zugeordnet wird. In der klassischen Aussagenlogik …   Deutsch Wikipedia

  • Baumkalkül — Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments… …   Deutsch Wikipedia

  • Berechnungsmodell — Dieser Artikel wurde auf der Qualitätssicherungsseite des Portals Mathematik eingetragen. Dies geschieht, um die Qualität der Artikel aus dem Themengebiet Mathematik auf ein akzeptables Niveau zu bringen. Dabei werden Artikel gelöscht, die nicht… …   Deutsch Wikipedia

  • Beth-Kalkül — Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments… …   Deutsch Wikipedia

  • Beth-Tableau — Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments… …   Deutsch Wikipedia

  • Beth-Tableaux — Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments… …   Deutsch Wikipedia

  • Beth Tableau — Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments… …   Deutsch Wikipedia

  • Beth Tableaux — Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments… …   Deutsch Wikipedia

  • KKNF — Als konjunktive Normalform (kurz KNF) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet. Inhaltsverzeichnis 1 Definition 2 Kanonische konjunktive Normalform 3 Bildung 4 Beispiel für die Bildung der KNF 5 …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”