www.wikidata.de-de.nina.az

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

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:

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

Somit sind folgende Aussagen möglich:

  1. ist die leere Klausel Element von , ist unerfüllbar und
  2. 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:

1)

(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.

  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 aus der Formel und bringt sie in die Skolemform.
  3. 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:

2)

Substitution und Vereinheitlichung

Die Formeln

und

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

und

die sich offensichtlich miteinander resolvieren lassen.

Folgende Ersetzungen sind möglich:

3a) Ersetze Variable durch Konstante:
3b) Ersetze Variable durch eine andere Variable:
3c) Ersetze Variable durch Funktion einer Variablen:

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:
4b) Verbotene Ersetzung:

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:

¬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 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

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

wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Die Resolution ist ein Verfahren der formalen Logik um eine logische Formel auf Gultigkeit zu testen Das Resolutionsverfahren auch Resolutionskalkul genannt ist ein Widerlegungsverfahren Statt direkt die Allgemeingultigkeit 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 durchgefuhrt werden Die Resolution ist eine der bekanntesten Techniken des Maschinengestutzten Beweisens Inhaltsverzeichnis 1 Das Resolutionsverfahren in der Aussagenlogik 1 1 Resolvente auch Resolvent 1 2 Beweis 1 3 Res Operator 2 Resolution und Pradikatenlogik 2 1 Problemstellung 2 2 Normalisierung 2 3 Substitution und Vereinheitlichung 2 4 Resolution pradikatenlogischer Klauseln 3 Beispiel 3 1 Ein logisches Ratsel 3 2 Das Ratsel in Klauselform 3 3 Die Auflosung 4 Terminierung und Komplexitat 5 Andere Kalkule im logischen Einsatz 6 Quellen 7 Literatur 8 WeblinksDas Resolutionsverfahren in der AussagenlogikResolvente auch Resolvent Seien C 1 displaystyle C 1 nbsp C 2 displaystyle C 2 nbsp Klauseln einer aussagenlogischen Formel die in konjunktiver Normalform vorliegt Gibt es ein Literal L displaystyle L nbsp welches in C 1 displaystyle C 1 nbsp positiv und in C 2 displaystyle C 2 nbsp negativ vorkommt ist die Vereinigung beider Klauseln ohne das positive und negative Literal L displaystyle L nbsp eine Resolvente auch der Resolvent C R displaystyle C R nbsp Das heisst insbesondere Gibt es kein komplementares Literal so gibt es auch keine Resolvente L C 1 displaystyle L in C 1 nbsp L C 2 displaystyle overline L in C 2 nbsp C R C 1 L C 2 L displaystyle C R C 1 setminus L cup C 2 setminus overline L nbsp Es darf immer nur genau ein Literal resolviert werden Je nach Ausgangsklauseln ist die Bildung verschiedener Resolventen moglich Anders notiert Aus A 1 A 2 A n B 1 B 2 B m A 1 displaystyle 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 nbsp wird auf die Resolvente A 2 A n B 1 B m displaystyle A 2 vee dots vee A n vee B 1 vee dots vee B m nbsp geschlossen Die Resolvente ist nicht aquivalent zu den Ausgangsklauseln Die Bedeutung der Resolvente liegt vielmehr darin dass die Ausgangsklauseln nur dann beide gleichzeitig erfullbar sind wenn auch die Resolvente erfullbar ist notwendige Bedingung Gelingt es die leere Klausel zu resolvieren die stets unerfullbar ist ist somit die Unerfullbarkeit der gesamten Formel gezeigt Beweis Da die Resolvente C R displaystyle C R nbsp eine notwendige Bedingung fur die Ausgangsklauseln C 1 displaystyle C 1 nbsp und C 2 displaystyle C 2 nbsp ist gilt C 1 C 2 C R displaystyle C 1 wedge C 2 rightarrow C R nbsp Man sagt C R displaystyle C R nbsp folgt aus C 1 displaystyle C 1 nbsp und C 2 displaystyle C 2 nbsp Hieraus folgt der Beweis zur Korrektheit der Resolution A 1 A 2 A n B 1 B 2 B m A 1 A 2 A 3 A n B 1 B 2 B m A 1 A 2 A n B 1 B 2 B m A 1 A 2 A 3 A n B 1 B 2 B m A 1 A 2 A n B 1 B 2 B m A 1 A 2 A 3 A n B 1 B 2 B m A 1 A 2 A 3 A n A 1 B 1 B 2 B m A 1 A 1 1 displaystyle begin aligned amp 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 amp 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 amp 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 amp 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 amp equiv neg A 1 vee A 1 amp equiv 1 end aligned nbsp Res Operator Das Ausfuhren eines einzelnen Resolutionsschrittes wird mit dem Res Operator notiert Res F F R displaystyle operatorname Res F F cup R nbsp wobei R displaystyle R nbsp eine Resolvente zweier Klauseln aus F displaystyle F nbsp istMit Res F n N Res n F displaystyle operatorname Res star F bigcup n in mathbb N operatorname Res n F nbsp bezeichnet man die Vereinigung aller moglichen Resolutionsschritte auf F displaystyle F nbsp Somit sind folgende Aussagen moglich ist die leere Klausel Element von Res F displaystyle operatorname Res star F nbsp ist F displaystyle F nbsp unerfullbar und ist die leere Klausel Element von Res F displaystyle operatorname Res star neg F nbsp ist F displaystyle F nbsp eine TautologieResolution und PradikatenlogikProblemstellung Fur interessantere Problemstellungen ist das Instrumentarium der Aussagenlogik nicht ausreichend Das Prinzip der Resolution sollte von der einfachen Aussagenlogik auf die Pradikatenlogik erster Stufe ausgeweitet werden konnen Neben logischen Literalen sind dabei zu berucksichtigen Variablen beispielsweise Zahlenvariablen ublicherweise mit Symbolen wie x displaystyle x nbsp und y displaystyle y nbsp bezeichnet die Quantoren displaystyle exists nbsp der Existenzquantor und displaystyle forall nbsp der Allquantor Konstanten beispielsweise 0 1 p displaystyle 0 1 pi nbsp ein und mehrwertige Funktionen ublicherweise mit Symbolen wie f x displaystyle f x nbsp oder g x y displaystyle g x y nbsp bezeichnet Ein durchaus typisches Beispiel fur eine pradikatenlogische Aussage ist 1 x y z K g a z y K g f a f z x displaystyle forall x exists y forall zK g a z y implies K g f a f z x nbsp Anmerkung Setzen wir g t u t u displaystyle g t u vert t u vert nbsp und K v w v lt w displaystyle K v w equiv v lt w nbsp so liefert uns die obige Formel die formal logische Definition der Stetigkeit der Funktion f displaystyle f nbsp im Punkt a displaystyle a nbsp Damit auf solche Aussagen die Resolution angewendet werden kann mussen 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 ahnelt Man bringt die zu widerlegende Formel in die Pranexform 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 displaystyle exists nbsp aus der Formel und bringt sie in die Skolemform Nun sind alle Variablen in der Funktion an Allquantoren displaystyle forall nbsp gebunden Trifft man die Ubereinkunft Konstanten und Variablen unterschiedlich zu bezeichnen beispielsweise Konstanten mit a b c a 1 a 2 a 3 displaystyle a b c a 1 a 2 a 3 dotsc nbsp und Variablen mit x y z x 1 x 2 x 3 displaystyle x y z x 1 x 2 x 3 dotsc nbsp dann kann auch auf die explizite Notation des Allquantors verzichtet werden Man lasst ihn ebenfalls weg und erhalt die Klauselform der Aussage 1 Beispielsweise lautet die Klauselform der Formel 1 aus dem vorigen Abschnitt 2 K g a z s x K g f a f z x displaystyle neg K g a z s x vee K g f a f z x nbsp Substitution und Vereinheitlichung Die Formeln P x displaystyle P x nbsp und P a displaystyle neg P a nbsp scheinen auf den ersten Blick nicht resolvierbar zu sein da sie sich in x displaystyle x nbsp und a displaystyle a nbsp unterscheiden Da die freie Variable x displaystyle x nbsp jedoch implizit ein Stellvertreter fur alle x displaystyle x nbsp ist darf unter anderem a displaystyle a nbsp fur x displaystyle x nbsp eingesetzt werden Man erhalt also die beiden Terme P a displaystyle P a nbsp und P a displaystyle neg P a nbsp die sich offensichtlich miteinander resolvieren lassen Folgende Ersetzungen sind moglich 3a Ersetze Variable durch Konstante P x displaystyle P x nbsp displaystyle rightarrow nbsp P a displaystyle P a nbsp 3b Ersetze Variable durch eine andere Variable P x displaystyle P x nbsp displaystyle rightarrow nbsp P y displaystyle P y nbsp 3c Ersetze Variable durch Funktion einer Variablen P x displaystyle P x nbsp displaystyle rightarrow nbsp P f y displaystyle P f y nbsp Die Ersetzung von Variablen in einem Literal muss in konsistenter Weise durchgefuhrt werden Wird eine Variable an einer Stelle durch einen Term ersetzt so muss dies innerhalb des Literals uberall geschehen 4a Korrekte Ersetzung P x f x displaystyle P x f x nbsp displaystyle rightarrow nbsp P a f a displaystyle P a f a nbsp 4b Verbotene Ersetzung P x f x displaystyle P x f x nbsp displaystyle nrightarrow nbsp P a f x displaystyle P a f x nbsp Sei x 1 x 2 x n displaystyle lbrace x 1 x 2 dotsc x n rbrace nbsp eine Menge von Variablen Sei t 1 t 2 t n displaystyle lbrace t 1 t 2 dotsc t n rbrace nbsp eine Menge von Termen die aus Funktionen Variablen oder Konstanten zusammengesetzt sein konnen Ein System S displaystyle S nbsp von Ersetzungen x 1 t 1 x 2 t 2 x n t n displaystyle lbrace x 1 rightarrow t 1 x 2 rightarrow t 2 dotsc x n rightarrow t n rbrace nbsp heisst 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 displaystyle L 1 P t 1 t 2 dotsc t n L 2 P u 1 u 2 dotsc u n dotsc L m P v 1 v 2 dotsc v n nbsp Literale uber demselben Pradikat P displaystyle P nbsp wobei die t i u i v i displaystyle t i u i dotsc v i nbsp wiederum Terme sind Eine Substitution S displaystyle S nbsp heisst eine Vereinheitlichung oder auch Unifikator von L 1 L 2 L m displaystyle L 1 L 2 dotsc L m nbsp wenn durch die Anwendung von S displaystyle S nbsp die Argumente aller Literale zur Ubereinstimmung gebracht werden das heisst wenn S L 1 S L 2 S L m displaystyle S L 1 S L 2 dotsb S L m nbsp Zwei Literale uber demselben Pradikat haben nicht notwendigerweise eine Vereinheitlichung Beispielsweise lassen sich P a displaystyle P a nbsp und P b displaystyle P b nbsp nicht vereinheitlichen wenn a displaystyle a nbsp und b displaystyle b nbsp unterschiedliche Konstanten sind Eine Vereinheitlichung S displaystyle S nbsp von Literalen heisst allgemeinste Vereinheitlichung wenn es fur jede andere Vereinheitlichung T displaystyle T nbsp dieser Literale eine Substitution V displaystyle V nbsp gibt so dass T S V displaystyle T S circ V nbsp Wenn eine Menge von Literalen eine Vereinheitlichung besitzt dann besitzt sie eine allgemeinste Vereinheitlichung Diese kann mit Hilfe eines relativ einfachen Algorithmus 2 ermittelt werden Resolution pradikatenlogischer Klauseln Mit diesem Instrumentarium kann das Resolutionsverfahren auf Aussagen der Pradikatenlogik ausgeweitet werden Seien C 1 C 2 displaystyle C 1 C 2 nbsp zwei Klauseln einer normalisierten pradikatenlogischen Aussage Ohne Beschrankung der Allgemeinheit darf vorausgesetzt werden dass diese keine ubereinstimmenden Variablen enthalten da sie durch einen Allquantor gebunden sind konnen wir gleichnamige Variablen in einer Klausel umbenennen auch wenn der Allquantor nicht mehr explizit geschrieben wird Seien L 1 displaystyle L 1 nbsp und L 2 displaystyle L 2 nbsp positive bzw negiert vorkommende Literale in C 1 displaystyle C 1 nbsp bzw C 2 displaystyle C 2 nbsp die eine allgemeinste Vereinheitlichung S displaystyle S nbsp besitzen Dann heisst C R S C 1 C 2 S L 1 S L 2 displaystyle C R S C 1 cup C 2 setminus S L 1 neg S L 2 nbsp ein binarer Resolvent von C 1 displaystyle C 1 nbsp und C 2 displaystyle C 2 nbsp Sei ferner C displaystyle C nbsp eine Klausel mit einer Teilmenge von Literalen die eine allgemeinste Vereinheitlichung S displaystyle S nbsp besitzt Dann heisst S C displaystyle S C nbsp ein Faktor von C displaystyle C nbsp Ein Resolvent zweier Klauseln C 1 C 2 displaystyle C 1 C 2 nbsp ist entweder ein binarer Resolvent von C 1 displaystyle C 1 nbsp und C 2 displaystyle C 2 nbsp oder ein binarer Resolvent von C 1 displaystyle C 1 nbsp und einem Faktor von C 2 displaystyle C 2 nbsp oder ein binarer Resolvent eines Faktors von C 1 displaystyle C 1 nbsp und C 2 displaystyle C 2 nbsp oder ein binarer Resolvent eines Faktors von C 1 displaystyle C 1 nbsp und eines Faktors von C 2 displaystyle C 2 nbsp Das Resolutionsverfahren fur pradikatenlogische Aussagen besteht darin so lange solche Resolventen zu erzeugen bis die leere Klausel erzeugt und damit der Widerspruchsbeweis erbracht ist 3 BeispielEin logisches Ratsel Wir wollen das Prinzip am Beispiel eines kleinen nicht wortlich zu nehmenden logischen Ratsels illustrieren Seit dem Altertum ist bekannt dass alle Athener klug 1 und alle Spartaner heldenmutig 2 sind Ausserdem ist bekannt dass ein profundes Misstrauen zwischen beiden Stadten herrscht so dass doppelte Stadtburgerschaften 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 Stadte 4 Der Forscher kam ins Gesprach mit den Herren Diogenes Platon und Euklid Mit ihren beruhmten Vorbildern hatten diese nur den Namen gemein Die Herren zogen kraftig ubereinander 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 Spitzzungigkeit blieben die drei Herren mit ihren Behauptungen bei der Wahrheit Wer kommt aus welcher Stadt Das Ratsel in Klauselform Wir setzen p fur Platon d fur Diogenes e fur Euklid Die Pradikate ist Athener ist Spartaner ist heldenmutig und ist klug bezeichnen wir mit A S H und K Wir ubersetzen 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 Auflosung 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 fur 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 gefuhrt 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 KomplexitatIm Falle der Aussagenlogik terminiert das Verfahren Es liefert in endlicher Zeit ein Ergebnis ob eine vorgelegte Aussage erfullbar ist Die Rechenzeit wachst im allgemeinen Fall und mit den derzeit bekannten Verfahren exponentiell mit der Anzahl der Literale Das Problem ist NP vollstandig 4 Im Falle der Pradikatenlogik terminiert das Verfahren stets mit dem korrekten Ergebnis wenn es auf eine unerfullbare Formel angewendet wird Bei einer erfullbaren Formel kommt es jedoch vor dass das Verfahren kein Ende findet Man spricht von Semi Entscheidbarkeit Ware es anders dann ware das Resolutionsverfahren ein Algorithmus um pradikatenlogische Formeln allgemein zu entscheiden was unmoglich ist da das Gultigkeitsproblem in der Pradikatenlogik nicht entscheidbar ist Andere Kalkule im logischen EinsatzBaumkalkul in gewisser Weise unter den Kalkulen der nachste Verwandte des Resolutionskalkuls axiomatische Kalkule Systeme naturlichen Schliessens Sequenzenkalkul Existential GraphsQuellen 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 Chang Chin Liang Lee Richard Char Tung Symbolic Logic and Mechanical Theorem Proving Academic Press 1973 ISBN 0 12 170350 9 S 77ff Chang Chin Liang Lee Richard Char Tung Symbolic Logic and Mechanical Theorem Proving Academic Press 1973 ISBN 0 12 170350 9 S 80 81 Haken A The Intractability of Resolution Theoretical Computer Science 39 1985 pp 297 308 LiteraturChang Chin Liang Lee Richard Char Tung Symbolic Logic and Mechanical Theorem Proving Academic Press 1973 ISBN 0 12 170350 9WeblinksVorlesungsskript von Habel und Eschenbach 2009 Fachbereich Informatik Universitat Hamburg mit anschaulichen grafischen Darstellungen PDF Datei 410 kB Vorlesungsskript von Bernhard Beckert 2006 Universitat Koblenz Landau PDF Datei 197 kB Logic for Computer Scientists von Ulrich Furbach Universitat Koblenz Landau Abgerufen von https de wikipedia org w index php title Resolution Logik amp oldid 197199391