Rechnergestütztes Beweisen

Übungen

Blatt	Thema	Download	Ausgabe	Abgabe
1	Sequenzenkalkül, PVS	blatt1.pdf	22.10.	29.10.
2	Klausifikation und Resolution; Tutch	blatt2.pdf ue2/aufgabe5.req ue2/aufgabe6.req	29.10.	05.11.
3	zChaff, Prädikatenlogik	blatt3.pdf ue3/pidgeon3.cnf ue3/Ord-stub.pvs	05.11.	12.11.
4	Normalisierung, Kripke-Modelle	blatt4.pdf	12.11.	19.11.
5	Unifikation, Skolemisierung, SPASS	blatt5.pdf ue5/ord.spass	19.11.	26.11.
6	Induktive Beweise: Sortieren	Angabe ue6/list.pvs ue6/insert.pvs	11.12.	17.12.
7	If-Ausdrücke, Carry-Lookahead-Adder	blatt7.pdf ue7/ifexp.pvs ue7/adder.pvs	17.12.	07.01.
8	Prädikatenlogik in Coq	blatt8.pdf ue8/per.v	14.01.	21.01.
9	Induktive Familien in Coq	blatt9.pdf ue9/transClos.v	21.01.	28.01.
10	Wiederholungsaufgaben

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: Mon Dec 17 18:49:15 CET 2007