FB18 - Das Forum für Informatik

fb18.de / Diplom Informatik / Unterbereich Grundstudium / Formale Informatik

F1: Aufgaben zu Herbrand-Dingsen?

F1: Aufgaben zu Herbrand-Dingsen? 2004-07-17 13:33
NaZo
Weiß jemand, wo es Aufgaben mit Musterlösung zu diesem Herbrand-Zeugs gibt, vielleicht aus'm letzten Jahr oder so?

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 10:31
MalagaNt
WS02/03 Aufgabenzettel 14. Allerdings fehlt mir da die Musterlösung. Wird doch aber sicher einer hier haben ?!

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 11:54
NaZo
Die kriegt man aber nicht mehr, oder? Könnte mir das jemand zu schicken?

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 14:05
Brokkoli
WS02/03 Aufgabenzettel 14.

wo findet man den? oder kannst du mir den mal schicken? 3scharfe@inf…

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 17:49
MalagaNt
http://www.malagant.net/tmp/Blatt14.pdf

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 19:09
Brokkoli
hm ok.. ich versuchs mal *g*
1.)
D(F1) = {c,h(c,c),h(h(c,c),c),h(c,h(c,c)),h(h(c,c),h(c,c))…}
E(F1) = {P(c,c),P(h(c,c),c),P(c,h(c,c)),P(h(c,c),h(c,c)),..}

D(F2) = {a,f(a),f(f(a)),f(f(f(a))),… }
E(F2) = {Q(a),Q(f(a)),Q(f(f(a))),… }

D(F3) = {a,c,f©,h(a,f©)}
E(F3) = {Q(h(a,f©))}

wie soll man eigentlich eine vollständige aufzählung machen? wie das in der aufgabe steht.. das geht doch eigentlich nur durch rekursive definition oder? wird da sowas verlangt?

2.)
F1:
A mit A(P) = {(h(c,c),h(c,c))}
F2:
A mit A(Q) = {(f(m))|m € D(D2)}
F3:
A mit A(Q) = {(h(a,f©))}

bei dieser aufgabe bin ich mir absolut nicht sicher, ob ich das auch nur annähernd richtig habe.. hab mich so irgendwie nach Folie 11[ 9 ] gerichtet..

wie löst man aufgabe 4? das krieg ich im moment garnicht hin..

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 20:22
georg
hm ok.. ich versuchs mal *g*
1.)
D(F1) = {c,h(c,c),h(h(c,c)),h(h(h(c,c))),…}
E(F1) = {P(c,c),P(h(c,c),c),P(c,h(c,c)),P(h(c,c),h(c,c)),..}

also h(h(c,c)) ist nicht im Herbrand-Universum! h ist ein zweistelliges Funktionssymbol und daher w�re z.B. h(h(c,c), h(c,c)) drin! Und in der Herbrand-Expansion wird immer in der kompletten Formel ersetzt und nicht nur in die Prädikatensymbole eingesetzt! Damit auch eine MEnge von Formeln entsteht, die äquivalent ist zur Formel in Skolemform. Zumindest hab ich das so verstanden.

Ich w�rde das so angeben:

[img]http://mokrates.de/cgi-bin/texstring?D_0(F_1)%3D%5C%7Bc%5C%7D[/img]

[img]http://mokrates.de/cgi-bin/texstring?D_%7Bi%2B1%7D(F_1)%3DD_i(F_1)%5Ccup%20%5C%7Bh(u%2Cv)%5Cmid%20u%2Cv%5Cin%20D_i(F_1)%5C%7D%20[/img]

[img]http://mokrates.de/cgi-bin/texstring?D(F_1)%3D%5Cbigcup_%7Bi%5Cge%200%7D%20D_i(F_1)[/img]

Und E(F_1) ist dann:
[img]http://mokrates.de/cgi-bin/texstring?%20E(F_1)%3D%5C%7BP(u%2Ch(v%2Cc))%5Crightarrow%5Cneg%20P(c%2Cw))%5Cmid%20u%2Cv%2Cw%5Cin%20D(F_1)%5C%7D[/img]



Aber das ist ja letztlich nur ein Umschreiben der Definition.
Wie ist die Aufgabe gemeint?

Edit: Klammer vergessen
Edit: Idee: vielleicht könnte man das schöner lösen, indem man ne _Ab_zählung angibt [img]http://www.fb18.de/gfx/15.gif[/img]

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 20:53
Brokkoli
hm ok.. ich versuchs mal *g*
1.)
D(F1) = {c,h(c,c),h(h(c,c)),h(h(h(c,c))),…}
E(F1) = {P(c,c),P(h(c,c),c),P(c,h(c,c)),P(h(c,c),h(c,c)),..}

also h(h(c,c)) ist nicht im Herbrand-Universum! h ist ein zweistelliges Funktionssymbol und daher w�re z.B. h(h(c,c), h(c,c)) drin!

ok so meinte ich das eigentlich auch (habs jetzt mal geändert)

Und in der Herbrand-Expansion wird immer in der kompletten Formel ersetzt und nicht nur in die Prädikatensymbole eingesetzt! Damit auch eine MEnge von Formeln entsteht, die äquivalent ist zur Formel in Skolemform. Zumindest hab ich das so verstanden.

danke, das hatte ich noch nicht so richtig verstanden ;)
was das wirkliche ziel der aufgabe war hab ich auch noch nicht wirklich verstanden..
ansonsten noch zur aufgabe 4 - wie würde man sowas lösen?

Re: F1: Aufgaben zu Herbrand-Dingsen? 2004-07-18 21:09
georg
ansonsten noch zur aufgabe 4 - wie würde man sowas lösen?

Du sollst hier zeigen, dass die Reflexivität aus den anderen Eigenschaften folgerbar ist. Da das hier mit Resolution gemacht werden soll, musst du die zu beweisende Aussage auf einen Unerfüllbarkeitstest zurückführen. Und Folgerungen führt man so auf einen Unerfüllbarkeitstests zurück:

Wenn man zeigen soll, dass [img]http://mokrates.de/cgi-bin/texstring?F_%7Bn%2B1%7D[/img] aus [img]http://mokrates.de/cgi-bin/texstring?F_1%2C%5Cldots%2CF_n[/img] folgt, zeigt man, dass
[img]http://mokrates.de/cgi-bin/texstring?F_1%20%5Cwedge%5Ccdots%20%5Cwedge%20F_n%20%5Cwedge%20%5Cneg%20F_%7Bn%2B1%7D[/img]
unerfüllbar ist.

Und dann wendet man prädikatenlogische Resolution an.