Rechnergestütztes Beweisen

Übungen

Achtung! Ab Blatt 4 ist die Abgabe jeweils schon am Dienstag vor 18 Uhr im Sekretariat Z1.05 oder in meinem Büro D1.09.

Blatt Thema Download Ausgabe Abgabe Rückgabe Lösung

1 Sequenzenkalkül, PVS Übungsblatt 1 20.10. 26.10. 27.10. loesung-b1.zip

2 Klausifikation und Resolution Übungsblatt 2 27.10. 02.11. 09.11.

3 zChaff, Prädikatenlogik Übungsblatt 3 pidgeon3.cnf Ord-stub.pvs 03.11. 08.11. 09.11. loesung-b3.zip

4 Unifikation, Skolemisierung, SPASS Übungsblatt 4 barbers.spass 10.11. 15.11. 16.11. loesung-b4.zip

5 Gleichheit in PVS Übungsblatt 5 17.11. 22.11. 01.12. loesung-b5.zip

6 Induktive Beweise: Sortieren Übungsblatt 6 24.11. 29.11. 01.12. loesung-b6.zip

7 Korrektheit von Merge-Sort Übungsblatt 7 mergesort.pvs 01.12. 06.12. 08.12. loesung-b7.zip

8 Theorien und Entscheidungsverfahren Übungsblatt 8 12.12. 19.12. 22.12.

9 Natürliches Schließen; Coq Übungsblatt 9 15.12. 20.12. 22.12. loesung-b9.zip

10 Fallstudien in PVS Übungsblatt 10 Dateien 22.12. 10.01. loesung-b10.zip

11 CTL, Fixpunkte und Model-Checking Übungsblatt 11 12.01. 17.01. 18.01. loesung-b11.zip

12 Model-Checking und Abstraktion Übungsblatt 12 19.01. 24.01. 27.01. loesung-b12.zip

13 Induktive Definitionen; Coq Übungsblatt 13 aufgabe33.v 27.01. 01.02.

Die Übungen dürfen auch in Gruppen bis zu zwei Personen bearbeitet werden. Werden gemeinschaftlich erarbeitete Lösungen getrennt eingereicht, dann muss bei beiden Fassungen aufgeschrieben sein, mit wem zusammen die Aufgabe gelöst wurde.

Andreas Abel

Last modified: Fri Jan 27 13:26:52 CET 2006