Moin moin,

ich habe mal ein paar Fragen und hoffe, dass der ein oder andere etwas dazu schreiben kann. [img]http://www.fb18.de/gfx/23.gif[/img]

Resolution grundsätzlich habe ich schon verstanden, also das braucht ihr mir nicht nochmal zu erklären, sondern nur auf die speziellen Fragen einzugehen. [img]http://www.fb18.de/gfx/10.gif[/img]

Der Link zum entsprechenden Kapitel im Skript ist:

http://www.informatik.uni-hamburg.de/WSV/f1/2002/VL-PDF/F1-08AL-Resolution.pdf

oder alternativ im Schöning 39ff. (AL) und 106ff. (PL)

(1) Stützmengenresolution

Wie genau geht denn das? Also ich nehme mir eine Teilmenge T der Klauslemenge F raus, so dass F\T erfüllbar ist. Woher weiss ich denn dann, welche Stützmenge ich mir genau nehme, die kann ich doch dann recht frei wählen oder?

Was ist der Sinn dieser Methode?

Und was soll mir das Beispiel sagen???


(2) Stützmengenresolution vs. lineare Rekursion

Wieso ist denn die lineare Resolution ein Spezialfall der Stützmengenresolution??? [img]http://www.fb18.de/gfx/5.gif[/img]


(3) Anwendung der versch. Resolutionsarten

Wofür verwendet man denn welche Resolution? Wo liegen die Vorteile der einzelnen Resolutionsarten, wo die Nachteile???


(4) Vollständigkeit

Einige Resolutionsarten sind bekanntermaßen nicht vollständig, welche praktischen Auswirkungen hat das denn nu' für mich, doch nur, dass ich evtl. in eine Sackgasse laufe, oder? Wenn ich mit einer nicht vollst. Resolution auf das gewünschte Ergebnis komme, gilt das doch ohne Einschränkungen, oder?


(5) Tipps zur Anwendung

Wie kommt ihr darauf welche Resolution nun gerade die richtige ist?

Also dann schonmal danke im Voraus für eure Hilfe und allen noch weiterhin schöne Pfingstferien.

[img]http://www.fb18.de/gfx/danke.gif[/img] [img]http://www.fb18.de/gfx/danke.gif[/img] [img]http://www.fb18.de/gfx/danke.gif[/img]

(1) Stützmengenresolution

Wie genau geht denn das? Also ich nehme mir eine Teilmenge T der Klauslemenge F raus, so dass F\T erfüllbar ist.

genau

Woher weiss ich denn dann, welche Stützmenge ich mir genau nehme, die kann ich doch dann recht frei wählen oder?

tja, von Zauberei kommt das nicht, das muss man schon wissen, damit man die Vorteile geniessen kann,
mit der Datenbank gibt es doch ein nachvollziehbares Beispiel dazu

Was ist der Sinn dieser Methode?

weniger mögliche Resolutionsschritte (da eingeschränkt)
-> schneller alle durch, schneller am Ziel

Und was soll mir das Beispiel sagen???

meinst du das mit der Datenbank?
das soll dir zeigen wie man auf so ein T kommen kann, ein Beispiel eben..

(2) Stützmengenresolution vs. lineare Rekursion

Wieso ist denn die lineare Resolution ein Spezialfall der Stützmengenresolution???

wenn die Menge T nur aus der Anfangsklausel K besteht sind doch
formal alle Eigenschaften der Stüzmengenresolution erfüllt
(falls ich mich gerade nicht verdenke)
-> also ist die lineare Resolution eine Stützmengenresolution,
da sie noch weitere Einschränkungen hat kann man sie durchaus
als 'Spezialfall' titulieren

die logische Verwandschaft erschliesst sich mir allerdings gerade auch nicht
(ich hab wieder einen Redestil drauf.. ;) )

(3) Anwendung der versch. Resolutionsarten

Wofür verwendet man denn welche Resolution? Wo liegen die Vorteile der einzelnen Resolutionsarten, wo die Nachteile???

alle verwendet man zur Resolution,
die verschiedenen Arten ermöglichen durch Einschränkung eine schnellere Lösung des Problems
und werden dort eingesetzt wo es geht, wo die Bedingungen erfüllt sind,

Vorteil: es geht schneller
Nachteil: bestimmte Bedingungen müssen vorher erfüllt werden

(4) Vollständigkeit

Einige Resolutionsarten sind bekanntermaßen nicht vollständig, welche praktischen Auswirkungen hat das denn nu' für mich, doch nur, dass ich evtl. in eine Sackgasse laufe, oder?

so siehts aus, das ist doch ein interessanter Punkt,
da muss man also aufpassen welche Resolution man wählt,

Wenn ich mit einer nicht vollst. Resolution auf das gewünschte Ergebnis komme, gilt das doch ohne Einschränkungen, oder?

jo

(5) Tipps zur Anwendung

Wie kommt ihr darauf welche Resolution nun gerade die richtige ist?

das sollte wirklich nicht dein Problem sein,
und ist auch gar nicht Thema in F1,

ich glaube bevor sich solche Fragen stellt
hat man schon jahrelang tausende Buchseiten zu diesem Thema gelesen,

in der Industrie oder Wissenschaft gibts dann sicher hochkomplexe Analysen/ riesige Programme und Auswertungen,
blah blah, ich spekuliere nur ;),

mit F1-Modellen, die auf eine Folie passen, wird das dann sicher nix mehr zu tun haben ;)

für F1-Übungen geht alles mit der normalen Resolution

Also erstmal danke für die schnelle und lange Antwort [img]http://www.fb18.de/gfx/6.gif[/img] jetzt ist mir fast alles klar…

tja, von Zauberei kommt das nicht, das muss man schon wissen, damit man die Vorteile geniessen kann,
mit der Datenbank gibt es doch ein nachvollziehbares Beispiel dazu

Das ist ja das Problem das Beispiel mit der Datenbank ist mir irgendwie nicht so ganz klar, vielleicht denke ich auch falsch da…
Wieso ist G'=T? Dann muss ja F' erfüllbar sein, aber woher weiss ich, dass in F' nicht doch noch etwas drin ist, das es unerfüllbar macht?

wenn die Menge T nur aus der Anfangsklausel K besteht sind doch
formal alle Eigenschaften der Stüzmengenresolution erfüllt

Ok soweit hab' ich nicht gedacht, das ist klar jetzt!

alle verwendet man zur Resolution,
die verschiedenen Arten ermöglichen durch Einschränkung eine schnellere Lösung des Problems
und werden dort eingesetzt wo es geht, wo die Bedingungen erfüllt sind,

Vorteil: es geht schneller
Nachteil: bestimmte Bedingungen müssen vorher erfüllt werden

Ja welche Bedingungen denn gerade? Bei P-, N- und Einheitsreso ist es schon klar, aber wie ist es z.B. mit linearer Resolution? Woher erkenne ich denn, dass es jetzt gerade super toll ist, diese anzuwenden??? [img]http://www.fb18.de/gfx/2.gif[/img]

das sollte wirklich nicht dein Problem sein,
und ist auch gar nicht Thema in F1

Ich hoffe, das sehen die Leute, die die Klausur zusammenstellen auch so [img]http://www.fb18.de/gfx/15.gif[/img] *lol*

Wenn man sich

http://3773.rapidforum.com/topic=101685916419

mal ansieht, scheint es aber doch zumindest in einer Übung aus den vergangenen Jahren drangekommen zu sein.

in der Industrie oder Wissenschaft gibts dann sicher hochkomplexe Analysen/ riesige Programme und Auswertungen,
blah blah, ich spekuliere nur ;),

Dann weiss ich ja schon was ich nach dem Studium mache *lol* [img]http://www.fb18.de/gfx/15.gif[/img]

Naja jedenfalls schonmal vielen Dank für die Hilfe, ich hoffe jemand weiss noch was zu den offen gebliebenen Fragen, besonders wann ich die lin. Resolution anwende.

[img]http://www.fb18.de/gfx/danke.gif[/img]

Das ist ja das Problem das Beispiel mit der Datenbank ist mir irgendwie nicht so ganz klar, vielleicht denke ich auch falsch da…
Wieso ist G'=T? Dann muss ja F' erfüllbar sein, aber woher weiss ich, dass in F' nicht doch noch etwas drin ist, das es unerfüllbar macht?

F' wird als erfüllbar angenommen, so ist die Datenbank designt worden,
darin stehen nur Sachen die sich gegenseitig bestätigen
oder nichts miteinander zu tun haben
(wenn man reinschreibt 'die Sonne ist gelb',
dann gibts später ne Fehlermeldung falls man zusätzlich
'die Sonne ist nicht gelb' reinzuschreiben versucht)

das ist eben so, gerade weil die Datenbank so eine tolle Eigenschaft hat
kann man nun Stützresolution darauf anwenden

Ja welche Bedingungen denn gerade? Bei P-, N- und Einheitsreso ist es schon klar, aber wie ist es z.B. mit linearer Resolution? Woher erkenne ich denn, dass es jetzt gerade super toll ist, diese anzuwenden??? [img]http://www.fb18.de/gfx/2.gif[/img]

ich könnte mir das als vorteilhaft vorstellen wenn man weiss,
dass eine bestimmte Klausel die kritische ist,
dass es bei ähnlichen Resolutionen oft an dieser gelegen hat
(ganz abstrakt gesprochen),

dann könnte man zunächst versuchen mit primär dieser Klausel
einen Widerspruch zu finden (also linear),

wenn ja, gut, nicht der schnellstmögliche Weg,
aber doch deutlich schneller als totale Breitensuche,

wenn nein, na dann nicht Glück gehabt,
dann vielleicht mit der zweitkritischsten versuchen
oder normale Resolution
(der Widerspruch kann ja auch innerhalb der restlichen Klauseln liegen)

(wobei ich es vorhin falsch formuliert habe,
das T ist nicht K sondern alle Klauseln (F) ohne K

denn F\T = F\(F\K) = K ist dann eine Klausel und erfüllbar)

Wenn man sich

http://3773.rapidforum.com/topic=101685916419

mal ansieht, scheint es aber doch zumindest in einer Übung aus den vergangenen Jahren drangekommen zu sein.

falls du die Aufgabe nicht hast:

Als Resolutionsstrategien stehen zur Auswahl:
P-Resolution, N-Resolution, lineare Resolution,
Stützmengenresolution und die Einheitenresolution.

Wie verhalten sich diese Strategien, wenn sie auf eine Hornformel
angewendet werden, bei der genau eine Klausel nur negative Literale enthält?
(So eine Formel entspricht einem Prolog-Programm und einer Anfrage.)
Vergleichen Sie das Verhalten der Strategien auch mit dem Markierungsalgorithmus.

oha, ja das ist was zum nachdenken,
na siehts ja in dem Thread dort, was schlauen Köpfen dazu einfiel..

…gerade weil die Datenbank so eine tolle Eigenschaft hat kann man nun Stützresolution darauf anwenden…

Ok, jetzt geht mir ein Licht auf [img]http://www.fb18.de/gfx/24.gif[/img]

…eine bestimmte Klausel die kritische ist…

Klingt einleuchtend [img]http://www.fb18.de/gfx/14.gif[/img]

wobei ich es vorhin falsch formuliert habe,
das T ist nicht K sondern alle Klauseln (F) ohne K

Hatte schon verstanden was du meinst [img]http://www.fb18.de/gfx/25.gif[/img]

oha, ja das ist was zum nachdenken,
na siehts ja in dem Thread dort, was schlauen Köpfen dazu einfiel..

Naja ich hoffe mal so ne Aufgabe wäre ein bisschen zu zeitraubend für eine Klausur und einen grundlegenden Einblick in die Arten der Resolution hab' ich jetzt ja dank dir auch. [img]http://www.fb18.de/gfx/28.gif[/img]

Also vielen Dank nochmal!