Wann/Wie substituieren?

JulM
Mausschubser
Mausschubser
Beiträge: 47
Registriert: 1. Okt 2009 19:25

Wann/Wie substituieren?

Beitrag von JulM » 5. Sep 2010 14:11

Hi,

Ich bin gerade noch dabei mir das Resolutionskalkül für FO-Formeln anzuschauen/Aufgaben durchrechnen.
Jetzt habe ich gerade die Aufgabe G1 der 5.Übung bearbeitet und dabei sind mir zwei Dinge aufgefallen, die ich noch nicht ganz verstehe leider.
Und zwar geht es um die Substitution, ich hatte sie bis jetzt immer nur so angewandt, dass ich vor der eigentlichen Resolution, die Klauselmenge durch Substitution verändere. Hier bei der Musterlösung ist es aber so gemacht, das einfach zwischendurch innerhalb einer Klausel substituiert wird.
Deswegen die zwei konkreten Fragen:
Wann darf ich substituieren?
Wie darf ich substituieren? Muss ich es immer auf die komplette Klauselmenge machen oder geht es auch auf eine einzelne Klauseln? ( Nehme ich zwar stark an, da es hier in der Musterlösung, ja auch so ist, aber lieber nochmal nachgefragt :P )

Edit: Natürlich bezieht sich meine Frage auf die dritte Formelmenge.

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Wann/Wie substituieren?

Beitrag von John » 5. Sep 2010 14:28

Ich nehme an, mit substituieren meinst du das Einsetzen von Konstanten für die Variablen? Dann ist die Antwort schlicht, dass in der Musterlösung das verallgemeinerte Resolutionsverfahren verwendet wurde, anstatt der GI-Resolution. Konkrete Grundinstanzen sind da nicht nötig. Siehe FO-Skript Seite 25. Dann versteh ich aber nicht, wo du in der Musterlösung überhaupt siehst, dass substituiert wird.
DON'T PANIC

JulM
Mausschubser
Mausschubser
Beiträge: 47
Registriert: 1. Okt 2009 19:25

Re: Wann/Wie substituieren?

Beitrag von JulM » 5. Sep 2010 14:49

John hat geschrieben:Ich nehme an, mit substituieren meinst du das Einsetzen von Konstanten für die Variablen? Dann ist die Antwort schlicht, dass in der Musterlösung das verallgemeinerte Resolutionsverfahren verwendet wurde, anstatt der GI-Resolution. Konkrete Grundinstanzen sind da nicht nötig. Siehe FO-Skript Seite 25. Dann versteh ich aber nicht, wo du in der Musterlösung überhaupt siehst, dass substituiert wird.
Dass das verallgemeinerte Resolutionsverfahren benutzt wurde, stimmt ja. Dieses meinte ich natürlich auch, hätte ich mich vielleicht konkreter ausdrücken müssen.
Allerdings meine ich nicht das Einsetzen, sondern die Substitution, diese wird ja auch im Beispiel auf S. 25 beschrieben.
Konkret bei der Musterlösung geht es mir um den Schritt:
\(\left\{\neg Rxfx \right\} \rightarrow \left\{\neg Rfxffx \right\}\)

in diesen Schritt, wird ja einfach x durch fx substituiert.

franzose
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 146
Registriert: 9. Okt 2009 00:08

Re: Wann/Wie substituieren?

Beitrag von franzose » 5. Sep 2010 15:18

wichtig ist, dass vor allen Klauseln ein "fuer alle x, y, ..." steht, also gilt das dann ja auch fuer ein konkretes x wie zB fx. Sonst duerfte man ja auch nicht mit Grundinstanzen resolvieren, denk dran dass man durch die Resolution immer Klauseln mitreinnehmen, die nichts an der Erfuellbarkeit aendern duerfen!

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Wann/Wie substituieren?

Beitrag von John » 5. Sep 2010 16:05

Aha, das meintest du. Gut, dass ich mir das selber anschaue, ich war mir der Funktion des allgemeinen Resolutionsverfahrens selber noch nicht ganz klar. Jedenfalls sehe ich das jetzt so: Die Anwendung des allg. Resolutionsv. spart einem die Arbeit, immer wieder neue Grundinstanzen herziehen zu müssen, und diese dann von ganz "oben" wieder durch x-maliges Resolvieren zu etwas nutzbarem zu "formen".

Angenommen, du hast eine Klausel \(\{Rxy, Qx\}\) und \(\{\neg Rxy, Qx, Px\}\). Dann ist daraus die Resolvente \(\{Qx, Px\}\). Jetzt kannst du hier x lustig substituieren, wie du willst, ohne die Korrektheit der Resolvente zu verfälschen. Im GI-Resolutionskalkül müsstest du sie für jede konkrete Grundinstanz neu herleiten. Soweit zum Sinn. Aber den hattest du ja schon verstanden, wie ich sehe.

Um deine Frage zu beantworten: Innerhalb der Klauselmenge kannst du die Klauseln einzeln substituieren, wie du willst. Innerhalb einer einzelnen Klausel muss diese Substituierung aber konsistent sein, da ja die gesamte Klausel jeweils allquantifiziert ist.
DON'T PANIC

JulM
Mausschubser
Mausschubser
Beiträge: 47
Registriert: 1. Okt 2009 19:25

Re: Wann/Wie substituieren?

Beitrag von JulM » 5. Sep 2010 16:29

John hat geschrieben: Um deine Frage zu beantworten: Innerhalb der Klauselmenge kannst du die Klauseln einzeln substituieren, wie du willst. Innerhalb einer einzelnen Klausel muss diese Substituierung aber konsistent sein, da ja die gesamte Klausel jeweils allquantifiziert ist.
Danke, das war mir doch noch ein wenig unklar, ob ich das so darf ;)
Ich hatte es so zuerst verstanden, das wenn in einer Klausel substituiert wird, auch in jeder anderen Klausel der Term ersetzt werden muss. Deswegen hatte mich auch die Lösung ein wenig verwundert.
Jetzt kann der Freitag kommen :D

Antworten

Zurück zu „Archiv“