Sequenzkalkülfrage

Benutzeravatar
Dennis
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 29. Sep 2008 21:15

Sequenzkalkülfrage

Beitrag von Dennis »

Bei Übung4 e.) versuche ich das ganze mit der Hand zu lösen (Pen&Paper).
Die Musterlösung ist ja in KeY gemacht, jedoch werden hier Regeln verwendet wie z.B. "instEx" oder "instAll".

Die erste Frage dazu wäre, wo finde ich diese Regeln bzw. was sagen sie aus?
Da sie nicht auf den Folien sind (afaik) -> sind diese Regeln dann in der Klausur erlaubt? Im Lab waren sie ja explizit verboten.


Sollte jemand die Aufgabe mit den Regeln von Folie 22/23 im Handout FOL-Calculus gemacht haben, würde ich mich über eine PM freuen :)
...fragt stellvertretend für alle Freunde...

Boddlnagg
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 10. Dez 2012 12:07

Re: Sequenzkalkülfrage

Beitrag von Boddlnagg »

Die Regel instEx entspricht im Prinzip exRight und instAll entspricht allLeft. KeY verwendet diese Regeln, wenn man per Drag&Drop eine Variable auf den Quantor zieht, um den Quantor zu instanziieren (daher der Name). In der Klausur sollt ihr (wie auch im Lab 3) stattdessen die Regeln exRight bzw. allLeft verwenden.

Antworten

Zurück zu „Archiv“