Mathematik online lernen im Mathe-Forum. Nachhilfe online

Startseite » Forum » Illustration und Beweis zum Resolutionskalkül

Illustration und Beweis zum Resolutionskalkül

Universität / Fachhochschule

Sonstiges

Tags: Beweis, Resolution, Sonstig

maulwurf2304 aktiv_icon

15:53 Uhr, 20.06.2021

Hallo zusammen,

ich darf eine Aufgabe zu einer Variante des Resolutionskalküls bearbeiten:

Hierbei startet man mit

i = 0

und

R_{0} = K (F)

, also der zur Formel

F

gehörigen Klauselmenge. Dabei wird die folgende Schleife wiederholt durchlaufen:

1. Man sucht in

R_{i}

nach einem Paar

(K_{1}, K_{2})

von Klauseln, deren Resolvente K3 nicht in

R_{i}

liegt.
2. Gilt

K_{3} = \emptyset

, so meldet man “F ist unerfüllbar” und beendet den Algorithmus.
3. Wenn ein solches Paar nicht gefunden werden kann, so meldet man “F ist erfüllbar” und bricht ab.
4. Andernfalls setzt man

R_{i + 1} = R_{i} \cup K_{3}

, erhöht

i

und geht wieder zu Schritt 1.
Betrachten Sie dazu wieder die Formel aus der vorigen Aufgabe:

F = ((B \lor C) \land C \land (\neg B \lor A) \land (B \lor \neg C) \land (\neg C \lor \neg A) \land B)

Nun zur genauen Aufgabenstellung:
1. Beschreiben Sie einem möglichen Ablauf des obigen Algorithmus bei dieser Formel. (In Schritt 1 können evtl. verschiedene Klauseln für die Resolution gefunden werden.) Illustrieren Sie den Lauf des Algorithmus, indem Sie auf ein Blatt Papier die während des Laufs des Algorithmus verwendeten Klauseln aufschreiben und Pfeile von Klausel

K_{1}

nach Klausel

K_{3}

und von Klausel

K_{2}

nach Klausel

K_{3}

zeichnen, falls

K_{3}

Resolvente von

K_{1}

und

K_{2}

ist und dies im Schritt 1 des Verfahrens bei einem Durchlauf benutzt wurde.

2. Ist F erfüllbar?

Meine Notizen zu dieser Aufgabe habe ich im Anhang hochgeladen und ich kam zu dem Schluss, dass

K_{3} = \emptyset

für

K_{1} = C, A

und

K_{2} = \neg C, \neg A

gilt und somit F unerfüllbar ist. Ist das so korrekt?

Zudem soll ich zeigen, dass bei der Variante des Resolutionskalküls stets

R_{i} \subseteq R e s^{i} (K (F))

gilt.
Wenn der Algorithmus die Ausgabe “F ist erfüllbar” in Schritt 3 liefert und dabei mit einer Klauselmenge

R_{i}

endet: Begründen Sie, dass dann sogar

R_{i} = R e s^{\infty} (K (F))

gilt.

Bei diesem Beweis habe ich noch Schwierigkeiten. Gilt nicht generell

R_{i} = R e s^{i} (K (F))

?

Für alle, die mir helfen möchten (automatisch von OnlineMathe generiert):
"Ich möchte die Lösung in Zusammenarbeit mit anderen erstellen."

Hierzu passend bei OnlineMathe:

Zu diesem Thema passende Musteraufgaben einblenden

maulwurf2304 aktiv_icon

16:18 Uhr, 20.06.2021

Hier nochmal das Bild, ich bin mir unsicher, ob das funktioniert hat.

maulwurf2304 aktiv_icon

17:49 Uhr, 20.06.2021

Anscheinend funktioniert das mit dem Bild nicht. Hier in Kürze mein Vorgehen:

Es gilt

R_{0} = K (F)

.
Als 1. nehme ich

K_{1} = B, C

K_{2} = \neg B, A

und

K_{3} = C, A

.
2. und 3. führt zu 4. und au

R_{1}

nehme ich

K_{1} = C, A

K_{2} = \neg C, \neg A

sowie

K_{3} = \emptyset

und F ist unerfüllbar.

Diese Frage wurde automatisch geschlossen, da der Fragesteller kein Interesse mehr an der Frage gezeigt hat.

1538429

1538419

	Status: nicht eingeloggt	Noch nicht registriert?