Seite 1 von 1

Sequenzkalkülfrage

Verfasst: 2. Apr 2014 15:54
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 :)

Re: Sequenzkalkülfrage

Verfasst: 2. Apr 2014 17:46
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.