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.
Induktion
Die Art von Induktion in GloIn ist leider etwas, was ich ueberhaupt nicht hinbekomme, kann mir vielleicht mal jemand die Induktion von diesem Blatt erklaeren?
https://fsi.informatik.uni-erlangen.de/repo_public/klausuren/gloin/2014-03-20_braindump.pdf
[i]Induktion (Aufgabe 6)
Wenn ich das richtig verstanden habe repraesentatieren X und Y auch Formeln. Nur verstehe ich auch nicht ganz was das X=Y da soll.
IV:
∀X.E(Φ)
(E(Φ) <=> Φ ist erfuellbar)
IA:
E(X) = T
T ist erfuellbar
IS:
Wenn E(Φ1) und E(Φ2) gilt, dann gilt auch E(Φ1^Φ2),E(Φ1vΦ2) und E(Φ1→Φ2)
d.h. (E(Φ) = T) => (E(∀X.Φ) = T) => (E(∃X.Φ) = T)
=> ∀X.E(Φ)[/i]
wie kaputt ist das?
Induktion-SS13
https://www8.cs.fau.de/_media/ss13:glolop:probeklausurss13.pdf
Induktion (Aufgabe 6) - SS13
[i]
z.z. Sei: k ⊨ o→v dann gilt: k ⊨ X[A↦o]→X[A↦v]
I.V.
(k ⊨ o→v) → (k ⊨ X[A↦o]→X[A↦v])
(X1 /\ X2)[A↦o] = X1[A↦o] /\ X2[A↦o]
(X1 / X2)[A↦o] = X1[A↦o] / X2[A↦o]
I.A.
Fall 1:
X ≠ A dann gilt k ⊨ X→X (X→X=TRUE)
Fall 2:
X = A dann gilt k ⊨ o→v
I.S.
Fall 1:
X1,2 ≠ A dann gilt (I.V.) X1 /\ X2 = X1 /\ X2
Fall 2:
X1,2 = A dann gilt (I.V.) o /\ o = o /\ o
Fall 3:
X1=A und X2≠A dann gilt (I.V.) o/\ X2 = o /\ X2
Fall 4:
X1≠A und X2=A nur X1=A und X2≠A dann gilt (I.V.) X1 /\ o = X1 /\ o[/i]
ist das noch kaputter?
induktion ist einfach bääääh
agreed, aber nicht hilfreich 
SS13 haben wir etwas anders gelöst als im PAD steht.
k erfüllt nen Term. dann erstmal nur den ersten teil umgeformt (ohne die implikation) und dann kam erst die implikation mit der I.V. ^^