Grundinstanzenresolution

radix89
Mausschubser
Mausschubser
Beiträge: 66
Registriert: 13. Apr 2011 13:45

Grundinstanzenresolution

Beitrag von radix89 » 23. Aug 2011 12:25

Hatten wir dieses Thema überhaupt gemacht?

Ich war in jeder VL und kann mich daran nicht erinnern.
Wie funktioniert das?

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: Grundinstanzenresolution

Beitrag von Domac » 23. Aug 2011 13:46

Servus,
ich habe den gleichen Verdacht, siehe hier: http://d120.de/forum/viewtopic.php?f=170&t=23203
Ich würde mir wünschen, dass sich mal irgendjemand der Verantwortlichen meldet... und mal eine kurze und knappe Aussage darüber treffen kann.
Gruß domac

PS.: Im Notfall einfach selbst aneignen. Habe ich auch getan. ;)
Extend my dropbox space (here).
Thanks!

bafnai
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 126
Registriert: 13. Apr 2011 06:36

Re: Grundinstanzenresolution

Beitrag von bafnai » 23. Aug 2011 20:49

Hallo,
die Grundinstanzenresolution wurde in der Vorlesung übersprungen und wenn ich mich recht entsinne, hat der Professor erwähnt, dass es für die Klausur nicht relevant ist.
Es ist auch auf den Wiederholungsfolien ausgeklammert (siehe https://www3.mathematik.tu-darmstadt.de ... nsatz6.pdf; Folien 109 und 111).
Die Reduktion von FO auf AL ist auch ausgeklammert und diese braucht man für GI-Resolution.

MfG bafnai

kain
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 30. Sep 2009 13:49

Re: Grundinstanzenresolution

Beitrag von kain » 24. Aug 2011 11:22

Eine Aufgabe zum Üben und zu Korrektur:


1) \(\forall x\, \exists y\, Rxy\)
2) \(\forall x\, \exists y\, Lxy\)
3) \(\exists x\, (Px \land\, \forall y\, (Lxy \rightarrow\, \neg Py)\\)
4) \(\forall x\, \forall y\, (Lxy \rightarrow\, Rxy)\)
5) \(\forall x\, \forall y\, ((Px \land\, Rxy) \rightarrow\, Py)\)

Es soll mit GI - Resolution die Unerfüllbarkeit gezeigt werden.

1.) Klauseln erstellen:

1) {Rxfx}
2) {Lxfx}
3) {Px} {\(\neg Lxy, \neg Py\)}
4) {\(\neg Lxy\)}
5) {\(\neg Px, \neg Rxy, Py\)}

2.) Umformen der Klauseln bzw. einfügen der Konstante c (x = fc, y = ffc):
1){Rfcffc}
2){Lfcffc}
3){Pc} {\(\neg Lfcffc, \neg Pfc\)}
4){\(\neg Lfcffc\)}
5){\(\neg Pc, \neg Rfcffc, Pfc\)}


3.) GI - Resolution:

{\(\neg Pc, \neg Rfcffc, Pfc\)} mit {Pc} = {\(\neg Rfcffc, Pfc\)} mit {Rfcffc} = {Pfc}
{\(\neg Lfcffc, \neg Pfc\)} mit {Lfcffc} = {\(\neg Pfc\)}

{Pfc} mit {\(\neg Pfc\)} = []


Richtig so?

Antworten

Zurück zu „Archiv“