Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Probeklausur ws14/15
Hallo 
Ich schreibe dieses Semester Gloin und wollte fragen,ob es wie in Glolop eine Probeklausur geben wird.
Liebe Gruesse
Eigelb
Hast du bestimmt schon gesehen, aber hier ist der Link zur Probeklausur:
https://www8.cs.fau.de/_media/ws14:gloin:probeklausurWS1415.pdf
Ich hätte auch gleich Fragen bzw. sehr einfache Lösungsansätze dazu und wollte der Übersichtlichkeit wegen nicht noch einen neuen Thread aufmachen und würde gerne Meinungen dazu hören.
Aufgabe 2 Prädikatenlogik
Ich hätte die Aufgabe so gelöst, bin aber komplett unsicher, ob man das so machen kann…
-
A ⊆ B ::= ∀X ∈ A. X ∈ B Hierzu denke ich, dass es nicht erlaubt ist das A und B in der Form in der Formel zu verwenden, da man sie ja vorher nicht wirklich definiert hat.
Alternativ: ∀X, A, B. (X ∈ A) → (X ∈ B) Das kommt mir aber auch sehr falsch vor… -
∀X, Y. ¬(P(X) = P(Y))
-
∀X.A. X ∈ P(A) → X ⊆ A
-
" Jede nichtleere Menge enthält ein Element, mit dem sie keine Elemente gemeinsam hat" Also es gibt keine zwei gleichen Elemente?
Aufgabe 3 Unifikation
“=” ≙ dem “=” mit dem Punkt drüber
{(g(X, h(Z)), Z) = f(g(h(Z), h(Z)), h(W))}
→ {g(X, h(Z)) = g(h(Z), h(Z)), Z = h(W)}
decomp
→ {X = h(Z), h(Z) = h(Z), Z = h(W)}
decomp
→ {X = h(Z), Z = Z, Z = h(W)}
decomp
→ {X = h(Z), Z = h(W)}
delete
→ {X = h(h(W)), Z = h(W)}
elim
=> mgu((g(X, h(Z)), Z) und f(g(h(Z), h(Z)), h(W))) = [ X |-> h(h(W)), Z |-> h(W)]
Aufgabe 4 Resolution (edit: Klammerung falsch gelesen)
(∀X∀Y∀Z. ((R(X, Y) ∧ R(Y, Z)) → R(X, Z))
∧ ∀X ∃Y. R(X, f(Y))
∧ ∀X. R(f(X), a))
→ ∀X.R(X, a)
≡ ¬ (∀X∀Y∀Z. (¬(R(X, Y) ∧ R(Y, Z)) ∨ R(X, Z))
∧ ∀X ∃Y. R(X, f(Y))
∧ ∀X. R(f(X), a))
∨ ∀X.R(X, a)
Formel negieren:
(∀X∀Y∀Z. (¬(R(X, Y) ∧ R(Y, Z)) ∨ R(X, Z))
∧ ∀X ∃Y. R(X, f(Y))
∧ ∀X. R(f(X), a))
∧ ∃X.¬R(X, a)
≡ (∀X∀Y∀Z. (¬R(X, Y) ∨ ¬R(Y, Z) ∨ R(X, Z))
∧ ∀X ∃Y. R(X, f(Y))
∧ ∀X. R(f(X), a))
∧ ∃X.¬R(X, a)
Pränexe Normalform bilden
≡ ((∀X∀Y∀Z∀B∃C. (¬R(X, Y) ∨ ¬R(Y, Z) ∨ R(X, Z)) ∧ R(B, f(C)) )
∧ ∀X. R(f(X), a))
∧ ∃X.¬R(X, a)
≡ ((∀X∀Y∀Z∀B∃C∀D∃E. (¬R(X, Y) ∨ ¬R(Y, Z) ∨ R(X, Z)) ∧ R(B, f(C)) ) ∧ R(f(D), a)) ∧ ¬R(E, a)
≡ ∀X∀Y∀Z∀B∃C∀D∃E. (¬R(X, Y) ∨ ¬R(Y, Z) ∨ R(X, Z)) ∧ R(B, f(C)) ∧ R(f(D), a) ∧ ¬R(E, a)
Skolemform bilden
≡ ∀X∀Y∀Z∀B∀D. (¬R(X, Y) ∨ ¬R(Y, Z) ∨ R(X, Z))
∧ R(B, f(g(X, Y, Z, B))) ∧ R(f(D), a) ∧ ¬R(h(X, Y, Z, B, D), a)
=> {{¬R(X, Y), ¬R(Y, Z), R(X, Z))}, {R(B, f(g(X, Y, Z, B)))},
{R(f(D), a)} {¬R(h(X, Y, Z, B, D), a)}}
Aufgabe 5: Formale Deduktion
0 || ∃X.∀Y. P(X, Y)
1 ||| c
2 |||| d ∀Y. P(d, Y)
3 |||| P(d, c) (∀ E) 2
4 ||| P(d, c) (∃ E) 0 - 3
5 ||| ∃X. P(X, c) (∃ I) 4
6 || ∀Y. ∃X. P(X, Y) (∀ I) 1 - 5
7 | (∃X.∀Y. P(X, Y)) → (∀Y. ∃X. P(X, Y)) (→ I) 0 - 7
Aufgabe 6 Induktion
https://fsi.informatik.uni-erlangen.de/forum/thread/11159-Probeklausur-WS13-Aufgabe-6-Induktion
Auch kleine Hilfen sind sehr willkommen
Es gibt auch ein Pad:
https://pad.stuve.fau.de/p/OdP3XLqgKb
und danke fuer A5), hat bei mir einen grossen Denkfehler korrigiert
Erst mal vielen Dank dass du dir die mühe gemacht hast dies alles online zu stellen, hilft mir persönlich sehr! 
Ich hätte eine Frage zur Aufgabe 4): Prädikatenlogische Resolution
… Fehlt da nicht noch am Ende die Resolution selbst?
Also im Sinne von versuchen mittels der Klauseln der Skolemform eine Leere Klausel zu bekommen, um dann sagen zu können ob es erfüllbar bzw. nicht erfüllbar ist ? :huh:
Ja
Also ich habe mich nun mal an den Resolutionsbeweis heran gewagt, bin mir aber nicht sicher ob das alles so zulässig ist.
Klauselform:
{¬R(X1, Y), ¬R(Y, Z), R(X2, Z))} b[/b],
{R(B, f(g(X, Y, Z, B)))} b[/b],
{R(f(D), a)} b[/b],
{¬R(h(X, Y, Z, B, D), a)} b[/b]
Resolutionsbeweis:
Resolution von (1) , (3) mit σ = [Y->f(D) , Z → a] liefert:
{¬R(X1, f(D)), R(X2, a))} b[/b]
Resolution von (5), (4) mit σ = [X2 → h(X,Y,Z,B,D)] liefert:
{¬R(X1, f(D))} b[/b]
Resolution von (6), (2) mit σ = [X1-> B , D → g(X,Y,Z,B)] liefert:
▮
Feedback (mit Erklärungen bei Fehlern) ist erwünscht!
Ich hab das bis dahin eigentlich fast genauso.
Ich hätte allerdings gedacht, dass die letzte Klausel einfach nur {¬R(E, a)} bleiben kann, weil doch der letzte ∃-Quantor nicht im Wirkungsbereich der ganzen Allquantoren liegt, oder?
Alles links vom „rechtesten“ Implikationspfeil in der Angabe steht ja in Klammern.
Oder sehe ich das falsch?
Hab ne Frage zu der Lösung kann man hier X in der ersten Zeile einfach durch X1 und X2 ersetzen? Weil wenn man die letzten Schritte vertauschen würde wäre dies gar nicht notwendig oder?
Also ungefähr so:
Resolution von (1) , (3) mit σ = [Y->f(D) , Z → a] liefert:
{¬R(X, f(D)), R(X, a)} b[/b]
Resolution von (5), (2) mit σ =[X->B , D-> g(X,Y,Z,B)] liefert:
{R(B,a)} (6)
Resolution von (6), (4) mit σ = [B → h(X,Y,Z,B,D)] liefert:
▮
Da bin ich mir selber nicht sicher, aber ich glaube es mal gesehen zu haben in einer Übung.
Ich glaube dass ist gar nicht zulässig wegen dem Occurs-check. Hier ersetzt du B unter anderem wieder durch B.
Ich hätte noch ne Frage zur Existenzquantifizierung von freien Variablen.
Hier mal ein Beispiel:
∀x∃z((¬p(x, y) ∨ q(z, z))
Die freie Variable y existenzquantifizieren:
∃y∀x∃z(¬p(x, y) ∨ q(z, z))
Skolemform:
∀x(¬p(x, a) ∨ q(f(x), f(x)))
Hier wird y zur Konstanten.
Wenn ich stattdessen aber bspw. folgendes hätte:
∀x∃z((¬p(x, x) ∨ q(z, y))
Wird der Existenzquantor ebenfalls vorne angestellt und wird y in dem Fall auch zur Konstanten? Oder geht man so vor:
Die freie Variable y existenzquantifizieren:
∀x∃y∃z(¬p(x, x) ∨ q(z, y))
Skolemform:
∀x(¬p(x, x) ∨ q(f(x), g(x)))
Ich danke für Antworten
Zu der Lösung von Sto:
Ich glaube nicht, dass du das mit x1 und x2 so machen kannst, habe das zumindest noch nie gesehen und bin der Meinung, dass innerhalb einer Klausel nicht substituiert werden darf.
Sonst könnte man das bei bla-'s Lösung auch einfach mit dem B machen. Werde auch gern eines besseren belehrt
Hat jemand zuverlässige Informationen, ob man in der Klausur wie in den vergangen Semestern alles in Papierform mitnehmen darf?
Oder hat jemand die Emailadresse des Profs? Finde auf der www8 Hompage nur die des Sekretariats.
Siehe Seite des Kurses
Hierzu eine Frage:
Nach welchen Regeln geht man, um zu entscheiden, an welche Stelle das ∃y kommt?
Ich hab das bis jetzt immer ganz primitiv in der Reihenfolge eingeordnet, wie die Variablen in dem Ausdruck vorkommen.
Regeln dazu kenne ich leider auch nicht. Weiß nur durch diese Aufgabehttp://formal.iti.kit.edu/~beckert/teaching/Logik-SS06/blatt10.pdf
bzw deren Lösung http://formal.iti.kit.edu/~beckert/teaching/Logik-SS06/loesung_blatt10.pdf, dass das so gemacht wird. 
also dein
Aufgabe 2)
2. ist irgendwie sinnlos: da steht ja afaik nur “fuer alle x,y x!=y”
Vorschlag:
∀xϵM1.(xϵM2)^∀yϵM2.(xϵM1) → M1 = M2
EDIT:
Ausserdem mein Ansatz zur A2\5.
∀T(¬∃XϵT (X!=T) fuer “eindeutigkeit” aka
for all T(eilmengen) do not exist an XϵT with X!=T) // denn wenn die Menge einelementig ist hat sie nur ein element und zwar sich selbst, also X=T
aber ich habe keine Ahnung wie man das mit der grossen Vereinigung schreiben soll, kann mir da vll. jemand einen Tipp geben?
Müsste die Klauselform hier nicht so aussehen?
{{¬R(X, Y), R(B, f(g(X, Y, Z, B))), R(f(D), a)},
{¬R(Y, Z), R(B, f(g(X, Y, Z, B))), R(f(D), a)},
{¬R(h(X, Y, Z, B, D), a)}}
mittlerweile habe ich das ganze nochmal durchdacht und wenn ich das „Lifting Lemma“ richtig verstanden habe dann darf man mittels einer Grundsubstitution
Variablen in einer Klausel umbenennen (natürlich einheitlich). Also dass was ich gemacht habe mit der Umbenennung von X zu X1 und X2 in einer Klausel ist nicht zulässig.
Aber was zulässig sein sollte ist die Grundsubstitution von (2) [X-> X1 , B->B1]
Somit ergibt sich die Klauselform:
¬R(X, Y), ¬R(Y, Z), R(X, Z))} b[/b],
{R(B1, f(g(X1, Y, Z, B1)))} b[/b],
{R(f(D), a)} b[/b],
{¬R(h(X, Y, Z, B, D), a)} b[/b]
Resolutionsbeweis wäre dann:
Resolution von (1) , (3) mit σ = [Y->f(D) , Z → a] liefert:
{¬R(X, f(D)), R(X, a)} b[/b]
Resolution von (5) , (2) mit σ = [X->B1 , D → g(X1,Y,Z,B1)] liefert:
{R(B1,a)} b[/b]
Resolution von (6), (4) mit σ = [B1 → h(X,Y,Z,B,D)] liefert:
▮
Bist du sicher, dass die Klauselform richtig ist? Oder ist mein letzter Post Quatsch?
Ich gebe niemandem eine Garantie,
aber du kannst ja gerne Schritt für Schritt zeigen wie du auf deine Klauselform kommst.