Also ich habe nun das F1 Skript und alle F1 Aufgaben durchgearbeitet und habe noch ein paar offene Fragen:

1.
Darf ich bei der Resolution auch 2 Literale weg resolvieren?
z.B. {-A, B, C},{A, -B} |-res {C}

2.
Wieso kann ich bei der Grundresolution bei der Bildung der Grundinstanzen auf eine Klausel verschiedene Grundsubstitutionen anwenden? Oder wieso kann ich überhaupt für jede KLausel eine andere Substition wählen? Ich müsste doch die Substitution auf die gesamte Formel anwenden. (Siehe Folie 12.8 F1-Skript)

Das wars erstmal.

1.
Darf ich bei der Resolution auch 2 Literale weg resolvieren?
z.B. {-A, B, C},{A, -B} |-res {C}

Definitiv nein. [img]http://mokrates.de/cgi-bin/texstring?((%5Cneg%20A%20%5Cland%20B%20%5Cland%20C)%20%5Clor%20(A%20%5Cland%20%5Cneg%20B))[/img] ist nicht erfüllbar, [img]http://mokrates.de/cgi-bin/texstring?C[/img] ist erfüllbar.

{-A, B, C} {A, -B}
\ /
{-B,B,C} oder {-A,A,C} also hätte man nicht wirklich was davon.

2.
Wieso kann ich bei der Grundresolution bei der Bildung der Grundinstanzen auf eine Klausel verschiedene Grundsubstitutionen anwenden? Oder wieso kann ich überhaupt für jede KLausel eine andere Substition wählen? Ich müsste doch die Substitution auf die gesamte Formel anwenden. (Siehe Folie 12.8 F1-Skript)

wenn du eine Klausel mit P(z) hast, dann ist z eine Variable und die zugehörige Formal Vz P(z), man hat die Formel also durch Normalisierung schon so gedreht dass es immer ein Allquantor ist der solche gebundenen Variablen bindet,

P(z) heißt P für alle z, also P(a), und auch P(b), sogar P©, P für alle Konstanten eben,
P gilt für sie alle, deshalb darf man mehrmals substituieren,

wieso sollte das stören?
welche Regel glaubst du dabei zu verletzten?

———-

schau dir dieses Beispiel an (ich hoffe ich kriege das noch hin mit der Resolution ;) )

F: Vx P(x) ^ (P(a) -> !P(b))

wie soll ein Computer wissen ob das nur wahr oder falsch ist?
in dem er stur nach Regeln arbeit, zum Beispiel mehrmals einsetzt

F x/a wird zu P(a) ^ (P(a) -> !P(b)), daraus folgt !P(b)

F x/b wird zu P(b) ^ (P(a) -> !P(b)), daraus folgt P(b)


aha, aus F folgt !P(b) sowie P(b), na dann ist F wohl unerfüllbar

solche Gedankenschritte werden korrekt formalisiert durch die Resolution nachgebildet

Aber in Folie 12.8 wird für verschiedene Klauseln einer Formel unterschiedliche Substitution angewendet. Und selbst auf ein und die selbe Klausel wird eine andere Subs. angewand, und dann mit allen erhaltenen Instanzen resolviert.

so ist das nun mal aus
Vx P(x) folgt P(a) UND P(b) usw.

man macht da kein stures Formeln umformen oder simples Variablen substiturieren,

nein das sind nur Hilfsmittel!, es wird viel mehr (anderes!) gemacht
hier wird richtig gearbeitet, hier werden Algorithmen beschrieben die aus alten Formeln neue generieren,

—————-

bei der normalen Resolution ist das noch einfach, da hat man (A v B) ^ (!A) -> B
das kann man noch recht gut mit normalen Umformungen beschreiben,


das Problem bei Vx P(x) ist das x eine unendliche Menge an Werten annehmen kann, aber nur ein paar davon interessieren zur Resolution,

tja ich kann da ewig weiter schreiben und dann sagst du am Ende wieder einen kleinen Satz (den gleichen!) 'aber da wird 2x substituiert'..

was soll ich denn darauf antworten? ;)
es ist erlaubt, fertig ;)

Aber in Folie 12.8 wird für verschiedene Klauseln einer Formel unterschiedliche Substitution angewendet. Und selbst auf ein und die selbe Klausel wird eine andere Subs. angewand, und dann mit allen erhaltenen Instanzen resolviert.

Dass man dabei korrekt inferiert, liegt daran, dass die Formel,
deren Unerfüllbarkeit man untersucht, genau dann unerfüllbar ist,
wenn es eine Struktur gibt, die Modell für die gesamte Herbrand-
Expansion ist. Das bedeutet insbesondere, dass eine solche
Struktur Modell für eine beliebige Teilmenge der Herbrand-
Expansion ist, also auch von jeder Konjunktion von Grundinstanzen.

Konkret bedeutet das: egal, wie du in einer Klausel eine
Grundsubstitution durchführst, erhälst du immer eine Klausel, die
irgendwo in E(F) vorkommt und somit von einem Modell für F wahr gemacht werden muss. Das kommt daher, dass jede Klausel mit
den anderen Klauseln UND-verknüpft wird und damit immer von
einem Modell für die Formel wahr gemacht werden muss. Also sind die
Resolutionsschritte korrekt.

so gesehen verstehe ich es auch nicht mehr ;)
(sorry)

Ich habs nun verstanden ;D

2.
Wieso kann ich bei der Grundresolution bei der Bildung der Grundinstanzen auf eine Klausel verschiedene Grundsubstitutionen anwenden? Oder wieso kann ich überhaupt für jede KLausel eine andere Substition wählen? Ich müsste doch die Substitution auf die gesamte Formel anwenden. (Siehe Folie 12.8 F1-Skript)

Das wars erstmal.

Um mal die Folie zu zitieren:

Bei der Bildung der Grundinstanzen können die Klauseln individuell betrachtet werden, da
die Konjunktion bei der Mengendarstellung sowieso aufgelöst wird.

D.h. die Formelmenge {A,B,C} bedeutet eigentlich
A ^ B ^ C (Konjunktive Normalform). Wenn ich jetzt
aber - über die Resolutionsregeln - herausfinde, dass D wahr ist
GENAU DANN wenn A und B wahr sind, dann kann ich auch schreiben, dass
A ^ B ^ C ^ D wahr ist, GENAU DANN wenn
A ^ B ^ C wahr ist.

Bei der Resolution wollen wir aber herausfinden, ob letzteres wahr
ist. Wenn wir nun aber von der längeren Konjunktion zeigen, dass diese
wahr ist (bzw. nicht wahr ist), dann gilt das wegen der Biimplikation
auch für die eigentliche Formel, die wir überprüfen wollen.
D.h. {A,B,C} ist äquivalent zu {A,B,C,D}für unsere Resolution.

Das heißt aber, dass durch die Resolution die Menge erweitert wird,
über die wir resolvieren! Und da wir beliebige Elemente der Menge
benutzen, um zu resolvieren, können wir auch beliebige Elemente
doppelt verwenden - sie verschwinden ja nicht.

Das ist übrigens exakt das gleiche Vorgehen wie bei der Aussagenlogik.