Blog as Art – Informatik, Webdesign Der Blog für N3rds – mit Stil

26Jan/125

Wie löse ich das Resolutionskalkül

In der Informatik befasst man sich auf grundlegender, mathematischer Ebene mit dem Problem Aussagen zu bewerten um daraus entsprechende Schlüsse ziehen zu können. Das Lösen eines Resolutionskalküls ist eine Möglichkeit um zu beweisen das eine Menge von aussagenlogischer Formeln gegenüber einer Annahme erfüllbar ist oder nicht.
Als Beispiel haben wir folgende Aussagen gegeben:

  1. Wenn Sony eine neue Konsole herstellt, dann auch Microsoft.
  2. Sony oder Nintendo haben eine neue Konsole hergestellt.
  3. Entweder OnLive oder Nintendo haben eine neue Konsole gebaut.
  4. Eine neue Konsole hat entweder Sony oder OnLive hergestellt.

Angenommen wird, dass OnLive keine neue Konsole hergestellt hat.

Aus den Vier Aussagen müssen wir nun mathematische Formeln erzeugen. Dazu müssen wir uns erst einmal überlegen welche Variablen von Bedeutung sind. Wir machen folgende Zuweisung:

S = Sony hat eine neue Konsole
M = Microsoft hat eine neue Konsole
N = Nintendo hat eine neue Konsole
O = OnLive hat eine neue Konsole

Das heißt wir können uns zu den Vier Aussagen nun auch Vier Formeln überlegen:

Die Erste Aussage sagt, dass nur, wenn Sony eine Konsole herstellt, dann bringt auch Microsoft eine raus. Das bedeutet, dass die gesamte Aussage nur dann falsch ist, wenn Sony eine Konsole hergestellt hat, aber nicht Microsoft. In allen anderen Fällen stimmt die Aussage. Diese Überlegung entspricht der Subjunktion (\rightarrow). Daraus ergibt sich also folgende Formel für die erste Aussage:

\alpha_1 = S \rightarrow M

Die Zweite Aussage ist offensichtlich eine einfache “Oder” Verknüpfung (\vee).

\alpha_2 = S \vee N

Aussage 3. und 4. haben den gleichen Aufbau. Sie sagen, dass entweder der eine oder der andere was macht. Dabei ist das “entweder” und das “oder” von wichtiger Bedeutung, denn das weist auf eine XOR-Verknüfung (\oplus) hin. Es ergibt sich also:

\alpha_3 = O \oplus N
\alpha_4 = S \oplus O

Um nun Ein Resolutionskalkül zu erzeugen, müssen wir die Formeln in einer Formelmenge M_\alpha zusammenfassen. Diese Formelmenge wird in Konjunktiver Normalform (KNF) verlangt. Das heißt wir müssen unsere Formeln dahin umwandeln. Die KNF schreibt vor, dass die einzelnen Teilformeln nur aus NOT und ODER-Verknüpfungen bestehen und diese per UND Verknüpft sind. Dafür gibt es ein Verfahren, dass immer funktioniert.

  1. Formeln nur mit \wedge, \vee, \neg darstellen
  2. Falls etwas wie \neg(\ldots) vorkommt, wird De-Morgan angewandt
  3. Ausmultiplizieren

Wenn wir diese Schritte durchführen erhalten wir immer KNF. Für unsere Formeln ergibt sich also folgendes:

\alpha_1 = S \rightarrow M = \neg S \vee M
\alpha_2 = S \vee N
\alpha_3 = O \oplus N = (O \wedge \neg N) \vee (\neg O \wedge N) = (O \vee N) \wedge (\neg O \vee \neg N)
\alpha_4 = S \oplus O = (S \wedge \neg O) \vee (\neg S \wedge O) = (S \vee O) \wedge (\neg S \vee \neg O)

Im nächsten Schritt muss die gesamte Formel formuliert werden. Diese ist einfach alle Formeln die wir bis jetzt haben per UND verknüpft.

\alpha = \alpha_1 \wedge \alpha_2 \wedge \alpha_3 \wedge \alpha_4
\alpha = (\neg S \vee M) \wedge (S \vee N) \wedge (O \vee N) \wedge (\neg O \vee \neg N) \wedge (S \vee O) \wedge (\neg S \vee \neg O)

Das Kalkül davon ist jetzt nur eine andere Schreibweise. Das heißt man klammert die Terme ein die mit \vee verbunden sind und ersetzt \vee und \wedge durch ein “,”.

M_\alpha = \{\{\neg S, M\}, \{S, N\}, \{O, N\}, \{\neg O, \neg N\}, \{S, O\}, \{\neg S, \neg O\}\}

Und jetzt kommen wir auch endlich zum eigentlichen Resolvieren. Wir wollen beweisen das \neg O gilt. Um das zu beweisen müssen wir die negierte Annahme (also einfach nur O) in die Formelmenge mit aufnehmen und R^* erzeugen. Das bedeutet, dass wir solange Resolvieren bis es nicht mehr geht. Wenn dann in der Menge ein \emptyset vorkommt, dann haben wir bewiesen, dass die Annahme stimmt.

Resolvieren bedeutet, dass wir alle Teilmengen (die inneren Klammern) miteinander vergleichen. Sobald sich ein (!!!) Element auslöscht, also negiert und nicht negiert vorliegt, dann fasst man alle anderen Elemente in einer neuen Menge zusammen (bsp: \{\{A, B\}, \{\neg A, C\}\} wird zu \{\{A, B\}, \{\neg A, C\}, \{B, C\}\}. Für unser Beispiel sieht das also folgendermaßen aus:

R(M_\alpha \cup \{O\}) = M_\alpha \cup \{O\} \cup \{\{M, N\}, \{O, M\}, \{S, \neg O\}, \{N, \neg O\}, \{N, \neg S\},
\{\neg N\}, \{S, \neg N \}, \{\neg S\}\}

Für R^2(M_\alpha) = R(R(M_\alpha)) wird die Prozedur dann genauso gemacht, nur das man das gesamte Verfahren auf die neue Menge anwendet. Wenn man das bis zum bitteren Ende fortsetzt, sodass man am Ende nichts mehr kombinieren kann, dann hat man R^* erzeugt.
Wenn jetzt ein \emptyset in der Menge vorhanden ist, dann ist bewiesen das die Formelmenge unter der Annahme erfüllbar ist und damit ist die Rechnung zu Ende.

Ihr seht, es ist also ein relativ rechen intensives Verfahren, deswegen gebe ich nochmal eine kleine Zusammenfassung:

  1. Variablen definieren
  2. Umwandeln der Formeln in KNF
  3. Negierte Annahme in das Kalkül aufnehmen
  4. Resolvieren (denkt dran, man darf nur resolvieren wenn genau ein Element negiert vorliegt)
  5. Wenn die Leere Menge vorliegt, dann ist die Annahme richtig.

Ich hoffe damit konnte ich einigen helfen. Wenn ihr Fragen habt, dann stellt sie einfach in den Comments.

hat dir dieser Artikel gefallen?

Dann abonniere doch diesen Blog per RSS Feed!

Kommentare (5) Trackbacks (0)
  1. Korrigier mal erstmal die offensichtlichen Fehler.

  2. Hallo Markus,
    zuerst einmal, ich finde deinen Beitrag gut. Vielleicht meint asdd: “Die Zweite Aussage ist offensichtlich eine einfache “Oder” Verknüpfung”. In der folgenden Klammer steht ein “und”.
    Ich hätte 2 Fragen:
    1. wie bekomme ich die Umformung der Antivalenz hin (ohne einfach auswendig zu lernen).
    2. zu 4. Heißt das, folgender Term {a, !b,!c} würde nie angefasst?

    Danke
    Thomas

  3. Hi Thomas,

    Ich danke dir für deine Anmerkung und den Fehler habe ich korrigiert. Was asdd gemeint hat, kann ich leider auch nicht sagen, aber aufgrund dieses ausführlichen Kommentar habe ich (wie man sieht) es auch nicht für nötig erachtet dazu Stellung zu nehmen.

    Bei deinen Fragen kann ich dir leider keine sicheren Antworten mehr geben, weil der Stoff einfach nach einem Jahr nicht mehr present genug ist. Was ich aber noch sagen kann ist, dass es bei Dingen wie der Antivalenz eine einfache Definition ist und deshalb leider auswenig gelernt werden muss.

    LG
    Marcus

  4. Um die Antivalenz in eine Formel die nur aus (!, v, &) besteht umzuwandeln, kannst du einfach dir die Wahrheitstabelle aufschreiben. Dann gehst du genauso vor, wie wenn du für eine Funktion die DNF oder KNF bilden möchtest.

    Für DNF:
    S N
    0 0 0
    0 1 1 (!S & N) v
    1 0 1 (S & !N)
    1 1 0
    =>
    (!S & N) v (S & !N) (S !v N)

    Für KNF

    S N
    0 0 0 (S v N) &
    0 1 1
    1 0 1
    1 1 0 (!S v !N)
    => (S v N) & (!S v !N) (S !v N)

    Deine andere Frage verstehe ich leider nicht, weil ich nicht weiß, woher du das (a, !b, !c) hast.


Kommentieren

Connect with Facebook

Noch keine Trackbacks.