Seite parallel anzeigen
Die Resolution
(Aussagenlogik Kapitel 7.2.3)Diese Seite nimmt Bezug auf
(Seite parallel anzeigen)
- Aussagenlogik: Aussagenlogische Beweisverfahren
- Aussagenlogik: Konjunktive Normalform
Die Resolution beweist die Gültigkeit einer Formel γ, indem !γ auf einen Widerspruch geführt wird und konstruiert so indirekte Beweise.
Da die Resolution mit Klauselmengen arbeitet, müssen wir zunächst definieren, was eine "Klausel" ist:
D.h. eine Klausel hat die Form {γ1, γ2, ..., γn} für ein beliebiges n>=0 und repräsentiert die Formel γ=γ1|γ2|...|γn.
Ein Randfall ist die leere Klausel {}. Diese repräsentiert die leere Disjunktion und als solches per Definition falsch, also den Widerspruch.
Jede Formel in konjunktiver Normalform kann leicht in eine Klauselmenge umgewandelt werden: die Konjunkte entsprechen den Klauseln der Menge und deren Disjunkte den Elementen der Klausel.
Die Resolution hat 1 Regel: die Resolutionsregel.
Der Resolutions-Kalkül hat folgende Eigenschaften:
Da die Resolution mit Klauselmengen arbeitet, müssen wir zunächst definieren, was eine "Klausel" ist:
Eine Klausel C ist eine menge von Literalen, die die Disjunktion ihrer Elemente repräsentiert.
Eine Klauselmenge ist eine Menge von Klauseln, die die Konjunktion ihrer Elemente repräsentiert.
Eine Klauselmenge ist eine Menge von Klauseln, die die Konjunktion ihrer Elemente repräsentiert.
D.h. eine Klausel hat die Form {γ1, γ2, ..., γn} für ein beliebiges n>=0 und repräsentiert die Formel γ=γ1|γ2|...|γn.
Ein Randfall ist die leere Klausel {}. Diese repräsentiert die leere Disjunktion und als solches per Definition falsch, also den Widerspruch.
Jede Formel in konjunktiver Normalform kann leicht in eine Klauselmenge umgewandelt werden: die Konjunkte entsprechen den Klauseln der Menge und deren Disjunkte den Elementen der Klausel.
Beispiel - Eine Formel und die entsprechende Klauselmenge
Betrachten wir die FormelKNF(γ)=(g_b1|!w_a1)&(g_b1|!w_b1)&(g_b1|!w_c1)&(g_b1|!w_b2)
- γ=!g_b1->!w_a1&!w_b1&!w_c1&!w_b2
Die entsprechende Klauselmenge K={ {g_b1,!w_a1}, {g_b1,!w_b1}, {g_b1,!w_c1}, {g_b1,!w_b2} }
Seien C und D Klauseln.
Wenden wir die Resolutionsregel auf 2 Klauseln C und D an, so sagen wir, wir resolvieren C und D.
Das Ergebnis der Resolutionsregel wird Resolventen genannt.
Eine (Resolutions-)Ableitung einer Klausel C aus einer Klauselmenge K ist eine Abfolge von Anwendungen der Resolutionsregel auf Klauseln aus K und vorhergehenden Resolventen.
Eine (Resolutions-)Widerlegung einer Klauselmenge K ist eine Ableitung der leeren Klausel aus K.
Die Resolutionsregel lautet:
C∪{a} {!a}∪D
C∪D
Das Ergebnis der Resolutionsregel wird Resolventen genannt.
Eine (Resolutions-)Ableitung einer Klausel C aus einer Klauselmenge K ist eine Abfolge von Anwendungen der Resolutionsregel auf Klauseln aus K und vorhergehenden Resolventen.
Eine (Resolutions-)Widerlegung einer Klauselmenge K ist eine Ableitung der leeren Klausel aus K.
Beispiel - Eine Ableitung im Resolutionskalkül
Wir wollenableiten:
- die Klausel {a}
- aus der Klauselmenge { C1={a,b,!c}, C2={!b,!c}, C3={!a}, C4={a,c} }
Beschreibung der Ableitungsschritte
- Wir resolvieren C1 und C2.
- Das Ergebnis resolvieren wir mit C3.
- Resolvieren wir das Ergebnis mit C4,
- erhalten die gewünschte Klausel.
Ableitung (fahre mit der Maus über die Klauseln, um etwas über ihre Herleitung zu erfahren)
{a,b,!c} {!b,!c} {a,!c} {!a} {!c} {c,a} {!a}
- Er hat keine Axiome.
- Er hat nur 1 Regel.
- Er ist vollständig und korrekt.
- zurück zu Der Hilbert-Typ-Kalkül
- zum Seitenanfang
- weiter zu
