Formale Systeme

Wahlpflichtvorlesung/Stammmodul im Wintersemester 2013/2014

Prof. Dr. Peter H. Schmitt
Dr. V. Klebanov, Dr. M. Ulbrich, C. Scheben

Praxisaufgabe 2: Theorembeweiser

In dieser Praxisaufgabe sollen Sie einen maschinellen Beweis für einen einfachen mathematischen Satz mit Hilfe des Theorembeweisers KeY erstellen.

Für die vollständige Lösung dieser Praxisaufgabe erhalten Sie 1,5 Bonuspunkte fur die Abschlussklausur (bitte beachten Sie die Erlauterung zu Bonuspunkten auf der Webseite zur Vorlesung).

Auch für unvollständige Teillosungen werden Punkte anteilig vergeben.

Material

• Webstart für die aktuelle KeY Version. Bitte beachten Sie, dass sich diese Version von der Version auf der Webseite unterscheidet.
• Das Aufgabenblatt zur Praxisaufgabe
• Einführung in Beweisen prädikatenlogischer Aussagen mit KeY
• addassoc.key - Aufgabendatei für Teilaufgabe 2 (Lemma 1)
• addcomm.key - Aufgabendatei für Teilaufgabe 2 (Lemma 2)
• multcomm.key - Aufgabendatei für Teilaufgabe 2 (Lemma 3)
• dist.key - Aufgabendatei für Teilaufgabe 2 (Lemma 4)
• eq.key - Aufgabendatei für Teilaufgabe 2 (Lemma 5)
• fib.key - Aufgabendatei für Teilaufgabe 2

Abgabe

Die Abgabe der Praxisaufgabe erfolgt über die Abgabe-Seite. Auf dieser müssen Sie sich beim ersten Betreten mit Ihrer Matrikelnummer registrieren.