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.
Allgemeiner Fragefred
Hi,
da ich keinen Plan von Glolop hab und auch bis jetzt keine Übungsmitschriften habe, suche ich mal hier im Forum nach Hilfe.
Schaue mir gerade die Fitch-Kalküle an und hab gleich mal versucht ein paar Übungsaufgaben zu lösen. Könnte da mal jemand drüber schaun?
(Übungsblatte 8, Aufgabe 1)
zu zeigen: ¬A→(A→B)
| ¬A A |
|---|
| A→B →E 6 |
| ¬A→(A→B) →E 1,7 |
zu zeigen: A→(B∧C)→(A→B)
| A→(B∧C) A |
|---|
| A→B →E 3,7 |
| A→(B∧C)→(A→B) →E 1,8 |
zu zeigen: A∧(B→¬A)→A∧¬B
| A∧(B→¬A) A |
|---|
| A ∧E1 1 |
| B→¬A ∧E2 1 |
| ¬B ¬I 8 |
| A∧¬B ∧I 3, 9 |
| A∧(B→¬A)→A∧¬B →E 1,10 |
Sieht richtig aus, bis auf eine Sache: Statt →I schreibst du immer →E. Ich korrigiere es mal beim ersten Beispiel:
| ¬A A |
|---|
| A→B →I 2 - 4 |
| ¬A→(A→B) →I 1 - 5 |
Gracias. Jo das ergibt Sinn.
Gleich mal die nächste Frage: (Sorry fürs spamen hier, bin irgendwie recht alleine mit meinem Glolop-Unwissen kommt mir so vor :D)
Aktuelle Probeklausur, Unifikationsaufgabe. Hab jetzt einfach mal den Martelli Montanari-Algo aus dem Skript genommen.
1.f(g(X, h(Z)), Z) = f(g(h(Z), h(Z)), h(W))
2.g(X, h(Z)) = g(h(Z), h(Z)), Z = h(W) (Gleichungssystem aufgedröselt)
3.X = h(Z), h(Z) = h(Z), Z = h(W) (Gleichungssystem weiter aufgedröseln)
4.X = h(Z), Z = h(W) (X=X Gleichungen gelöscht)
=> o= [X->h(Z), Z->h(W)] (Meine sich daraus ergebende Substitutionsabbildung)
5. h(Z) = h(Z), h(W) = h(W) (Abbildung auf mein Gleichungssystem anwenden)
6. (X=X Gleichungen gelöscht)
Fertig da E leer. Dadurch ist o = [x->h(Z), Z-> h(W)] mein MGU.
Die Lösung würde ich mal sagen stimmt ja oder? Weiss hald nicht welche Notation der Lehrstuhl eigentlich haben will.
Von 4. auf 5. ist ein Fehler. Du müsstest eine der beiden Gleichungen wählen (und zwar die, deren linke Variable im Rest vorkommt, siehe X \in Vars(S) im Skript) und dann die daraus Entstehende Substitution nur auf den Rest des Gleichungssystems anwenden, aber nicht auf die Substitutionserzeugende Gleichung.
Also du meinst wenn ich folgendes habe:
X=h(Z), Z=h(W)
Dann nehme ich das X = h(Z) und substituiere es zu X = h(h(W)) oder wie? Und wie soll ich dann weiter machen?
Ja genau, und dann bist du schon fertig, du hast die Gleichungsmenge: {X = h(h(W)), Z = h(W)} keine Regel ist mehr anwendbar, also bildest du den mgu: [X → h(h(W)), Z → h(W)]
Hi hi,
mal noch ne Frage zur formalen Deduktion in der Prädikatenlogik.
Wenn ich folgendes als Prämissen habe:
∀X.(Prädikat1(X) → Prädikat2(X))
∀Y.(Prädikat3(Y) ∧ Prädikat4(Y))
Darf ich dann bei den Fitch-Kalkülen die Allquantor-Eliminierung unter einer gemeinsamen Konstante c machen? Eigentlich schon oder? Würde dann so aussehen:
Prädikat1(c) → Prädikat2(c)
Prädikat3(c) ∧ Prädikat4(c)
Wenn ich sowas habe: ∀X∀Y.P(…) dann ist es ja klar, dass das nicht geht. Bin mir aber bei dem obigen Beispiel nicht ganz sicher.