Hallo Leute.

Ich habe enorme Schwierigkeiten, Resolution zu verstehen.
Kann mir jemand einmal die Technik dahinter im Detail erklären. Aus dem Skript wrd ich nämlich auch nicht schlau.
Es wäre nett, wenn ihr auch ein Beispiel anhängen könntet, wo ihr die Schritte erklärt, die ihr gemacht habt.
Alles was ich soweit verstanden habe ist, das man mit Resolution die Erfüllbarkeit einer Klauselmenge prüfen kann (ich glaube es müssen Hornklauseln sein). Ich habe sogar schon mal ein Beispiel versucht, aber ich scheitere immer an bestimmten Stellen, an denen mir einfach die Reglen fehlen. Zum Beispiel weiss ich überhaupt nicht, wann ich welche klauseln ignorieren kann (auch hierzu wäre ein Beispiel sehr hilfreich).

Falls ich nach eurer Antwort keine Rückfragen mehr haben sollte, bedanke ich mich im Vorraus und wünsche einen guten Start ins neue Semester.

Zunächst einmal ist Resolution ein Verfahren, dass auf Unerfüllbarkeit testet. Wenn man Allgemeingültigkeit testen will, muss man die zu prüfende Formel negieren und dann die Resolution an der negierten Formel durchführen.

Man benötigt eine Formel in KNF. Diese schreibt man für die Resolution häufig als Klauselmenge.
In jedem Schritt bildet man aus 2 Klauseln eine Resolvente (neue Klausel), indem man alle Literale in die neue Klausel übernimmt, die entweder in positiver oder negierter Form in den beiden Ursprungsklauseln vorkommen. Literale, die positiv und negativ vorkommen, fallen weg. Dabei darf in jedem Schritt nur ein Paar komplementärer Literale entfernt werden. Genau dann, wenn man als Resolvente beliebiger Klauseln die leere Klausel erhält, ist die Formel unerfüllbar. (Du kannst also alle Klauseln ignorieren, die du nicht brauchst. Das liegt daran, dass zwischen den Klauseln Konjunktionen stehen und für beliebige Formel A ((0 und A)=0) gilt.)

Mal ein Beispiel (Übungsaufgabe vom letzten Jahr):
[img]http://14-04-78.tripod.com/informatik/resolution.jpg[/img]
- mit -E aus Klausel2 E aus K1 eliminieren. übrig bleiben C,A in Resolvente 1
- mit -E aus K2 E aus K3 eliminieren. übrig bleibt -B in R2
- mit -B aus R2 B aus K4 eliminieren. -C,A in R3
- mit -B aus R2 B aus K5 eliminieren. -A in R4
- mit R1 und R3 C elimieren. A in R5
- R4 und R5 ergeben zusammen die leere Klausel.
Unerfüllbarkeit ist nachgewiesen!

Zunächst einmal ist Resolution ein Verfahren, dass auf Unerfüllbarkeit testet. Wenn man Erfüllbarkeit testen will, muss man die zu prüfende Formel negieren und dann die Resolution an der negierten Formel durchführen.

der 2. satz gilt für tautologien,
erfüllbare formel bleiben durch negation immernoch erfüllbar,
es ist da egal welche der beiden formeln man durch die resolution schickt,
wenn bei der resolution der punkt erreicht wird, dass im aktuellen resolutionsschritt genau die gleiche klauselmenge wie im vorherigen schritt herauskommt (also keine neue mehr hinzu) dann kann man mit 'erfüllbar' aufhören,

In jedem Schritt bildet man aus 2 Klauseln eine Resolvente (neue Klausel), indem man alle Literale in die neue Klausel übernimmt, die entweder in positiver oder negierter Form in den beiden Ursprungsklauseln vorkommen. Literale, die positiv und negativ vorkommen, fallen weg.

nicht ganz, man sucht sich ein komplementäres paar (also z. b. A und -A (= not(A)), entfernt das eine literal aus der einen klausel und das komplementäre aus der anderen und wirft den rest zusammen,

richtig:
{A,-A} {A,-A} res-> {A,-A}

nicht richtig:
{A,-A} {A,-A} res-> leere klausel

Ups. schnell mal korrigieren, damit keiner was falsches lernt.

hmm, nun noch mein roman zum thema ;)

mist 5600 zeichen und nur 5000 sind in einem posting erlaubt, dann eben gestückelt ;)

lies ruhig auch mal die topics im bereich Formale Informatik
zu blatt 9 & 10

F1 - Aufgabenzettel 10
F1 - Aufgabenzettel 9



resolution:

ziel für ALLE formeln (nicht nur hornformeln):

unerfüllbarkeit einer formel beweisen (leere klausel),

oder allgemeingültigkeit, einfach schauen ob negierte
formel unerfüllbar ist, dann ist ausgangsformel tautologie,

oder erfüllbarkeit, wenn nach einiger resolutionszeit keine
neuen klauseln mehr resolviert werden, ist die formel erfüllbar,
kann allerdings bei grossen formeln uneffizient lange dauern


prinzip:
umwandlung der formel in spezielles aussehen
(KNF, konjugierte normalform, dann äqivalente mengendarstellung)
und dann durch einfache logische umformungen neue
teilformeln hinzugewinnen, FOLGERN,
das funktioniert alles auch ohne je von resolution gehört zu
haben, mit dem verfahren gehts aber einfacher, übersichtlicher,
sogar vom pc ausführbar (algorithmus halt),

ist F die ausgangsformel und hat man eine neue klausel K
richtig gefolgert, so gilt
F -> K
und damit auch
F == F AND K
ist K also unerfüllbar (die leere klausel symbolisiert das),
dann ist ja auch 'F AND K' unerfüllbar, damit auch F unerfüllbar,
fertig


beispiele zur resolutionsbildung:

formel A AND -A ('-' heisst not(A) )

normaler weg:
da kommt man durch denken drauf,
oder schaut in bekannte umformungsregeln und sieht:
formel UND negierte formel können wohl nicht beide
gleichzeitig wahr sein, also unerfüllbar

resolution:
mengendarstellung: {{A},{-A}}

{A} {-A} res-> LK (leere klausel),

aus den beiden linken klauseln wurde durch resolution die
LK gefolgert (nach den regeln der resolutionsbildung),

damit ist A AND -A unerfüllbar ohne langes nachdenken



anderes beispiel (steht auch schon in irgeneinem anderen topic ;) ):

F = (A OR B OR -D) AND (A OR B OR D)

kann man vielleicht schon sehen, dass F erfüllbar ist,
aber bisschen resolvieren kann nicht schaden ;)

erst mal normaler weg, da kommt man durch einige umformungen
zu etwas einfacherem:

F = (A OR B OR -D) AND (A OR B OR D)
== [ (A OR B) AND (A OR B OR D) ] OR [ -D AND (A OR B OR D) ]
== (A OR B) OR [ (-D AND (A OR B)) OR (-D AND D) ]
== (A OR B) OR [ -D AND (A OR B) ]
== (A OR B)

also auch F -> (A OR B)

resolution macht hier exakt das gleiche, nur schneller

{{A,B,-D} , {A,B,D}}

{A,B,-D} {A,B,D} res-> {A,B}

schon fertig,
wieder wurde eine neue klausel gefolgert,
diese ist erst mal nicht die leere klausel,
aber es gilt wiederum F -> (A OR B),
und damit auch F == F AND (A OR B),

dies bedeutet: wenn F AND (A OR B) unerfüllbar wäre, wäre auch F unerfüllbar

jetzt kann man mit F AND (A OR B) weitermachen,
ergibt die klauselmenge {{A,B,-D} , {A,B,D}, {A,B}}

und da kann man nur wieder
{A,B,-D} {A,B,D} res-> {A,B}
folgern,

also kommt nix neues hinzu,
damit ist bewiesen, dass die formel erfüllbar ist,

ohne resolution durch logische umformungen wär erfüllbarkeit
wohl nicht zu beweisen, da muss man schon eine wahrheitstafel bemühen,



anderes beispiel:

noch etwas komplizierter

F = (B OR A OR C) AND (-A OR C)


normaler weg:
durch formelumformungen kommt man zu

F == [(B OR A OR C) AND -A] OR [(B OR A OR C) AND C]

== ((B AND -A) OR [(A OR C) AND -A]) OR ([(B OR A) AND C] OR (C AND C))

== [(B AND -A) OR (C AND -A)] OR C

== (B AND -A) OR C

-> (B OR C)

ein etwas verrückter schritt, aber auch richtig


resolution:
{{B,A,C},{-A,C}}

{B,A,C} {-A,C} res-> {B,C}

sicher einiges übersichtlicher

in beiden fällen gilt:
F == F AND (B OR C)

gewinn: man kann in der nächsten resolutionsrunde die klausel {B,C} mitverwenden,

hier sinds wieder so wenig klauseln,
das beim nächsten schritt nix neues hinzukommt, also erfüllbar

teil 2:


kompletteres beispiel aus dem aktuellen blatt 10:

F = AND (A <-> C) AND (B -> A)

normaler weg:
da möchte ich nicht wissen, was man da auf dem normalen weg
alles anstellen kann..


resolution:

KNF: (B OR A OR C) AND (-A OR C) AND (-C OR A) AND (-B OR A)

km (klauselmenge): {{B,A,C},{-A,C},{-C,A},{-B,A}}

erster resolutionsschritt, nur ausgangsklauseln verwenden,
alles mögliche resolvieren:

{B,A,C} {-A,C} res-> {B,C}
{-A,C} {-C,A} res-> {-A,A}
{-A,C} {-C,A} res-> {-C,C}
{-A,C} {-B,A} res-> {-B,C}
{B,A,C} {-C,A} res-> {B,A}
{B,A,C} {-B,A} res-> {C,A}

danach km: {{B,A,C},{-A,C},{-C,A},{-B,A}, {B,C},{-A,A},{-C,C},{-B,C},{B,A},{C,A}}

2. resolutionsschritt:

da kann man jede menge resolutionen machen
(der pc müsste auch alle möglichen durchführen), aber nur

{B,C} {-B,C} res-> {C}
{B,A} {-B,A} res-> {A}

sind interessant, sonst kommen nur bereits bekannte raus

danach km: {{B,A,C},{-A,C},{-C,A},{-B,A}, {B,C},{-A,A},{-C,C},{-B,C},{B,A},{C,A},
{C},{A}}

hier kommen überhaupt keine neuen mehr raus, also ist die formel erfüllbar,



weiss man dagegen, wie man zur LK kommt, brauch man nicht alle
vorhandenen klauseln verwenden und auch nicht alle möglichen
klauseln resolvieren/ folgern,
man verwendet eben nur die, die man benötigt, den rest ignoriert man

beispiel:

F = AND (A <-> C) AND (B -> A) AND (-A)

KNF: (B OR A OR C) AND (-A OR C) AND (-C OR A) AND (-B OR A) AND (-A)

km: {{B,A,C},{-A,C},{-C,A},{-B,A},{-A}}

da schreibt man dann üblicherweise nur die gebrauchten
resolvierungen auf

{B,A,C} {-C,A} res-> {B,A}

{B,A} {-B,A} res-> {A}

{A} {-A} res-> LK, also unerfüllbar

also ist aufgabe 1a nun erfüllbar ???

scheint so, nicht wahr ;)

ich kann mich ja auch irren..