Formale Systeme
Vorlesung im Wintersemester 2014/2015
Prof. Dr. Bernhard Beckert (BB)
Thorsten Bormer (TB),
Dr. Vladimir Klebanov (VK),
Dr. Mattias Ulbrich (MU)
Praxisaufgabe 2: Theorembeweiser
In dieser Praxisaufgabe sollen Sie einen maschinellen Beweis für einen einfachen mathematischen Satz mit Hilfe des Theorembeweisers KeY erstellen.
(Anklicken für ein größeres Bild)
Für die vollständige Lösung dieser Praxisaufgabe erhalten Sie 20 Übungspunkte für die Abschlussklausur (bitte beachten Sie die Erlauterung zu Übungspunkten auf der Webseite zur Vorlesung).
Auch für unvollständige Teillösungen werden Punkte anteilig vergeben.
Material
- Bitte verwenden Sie in jedem Fall die KeY-Version von dieser Seite und nicht die Versionen auf den Seiten des Tools.
- Webstart für die aktuelle KeY Version. Bitte beachten Sie, dass sich diese Version von der Version auf der Webseite unterscheidet.
- Java Archive (
KeY.jar) für die aktuelle KeY-Version zum Herunterladen. Bitte beachten Sie, dass sich diese Version von der Version auf der Webseite unterscheidet.
Ausführen:java -jar KeY.jar - Das Aufgabenblatt zur Praxisaufgabe
- Einführung in Beweisen prädikatenlogischer Aussagen mit KeY
ZeroPrefix.java- Skelettdatei für Teilaufgabe 2
Abgabe
Die Abgabe der Praxisaufgabe erfolgt Über unsere Seiten im ILIAS-Portal.
Prof. Dr. Bernhard Beckert
Für diese Webseite: Dr. Mattias Ulbrich