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.
Lsg. Ansatz zur Altklausur Aufgabe 6 von WS1617
Aufgabenstellung zu finden hier: https://fsi.cs.fau.de/git_public/braindumps/gloin/2017-04-04/gloin_2017-04-04_braindump.pdf
Mein Lösungsvorschlag im Stile alter Lösungen, siehe Anhang. (Feedback durchaus erwünscht.)
Attachment:
Aufgabe 6 - Induction - 4.4.17.pdf: https://fsi.cs.fau.de/unb-attachments/post_152430/Aufgabe 6 - Induction - 4.4.17.pdf
Erst mal danke, für die übersichtliche Lösung.
Eine Frage: Was ist da die Induktionsvorraussetzung?
In Zeile 6 nutze ich jeweils Zeile 2 und 3 - ich nehme an, dass die Aussage für E_1, E_2 bereits bewiesen ist. Wenn dem so ist, dann ist sie auch für E mit E = and(E_1, E_2) wahr und komme dann damit zu Zeile 8. Beachte, dass die 4-7 auf Umgebung n_1 arbeiten, 8-9 auf Umgebung n_2.
Die IV schafft den Übergang, dass Aussage für n_1 wahr die Aussage wahr für n_2 impliziert.
Für or kann man das sehr ähnlich machen.