Technische Universität München, Fakultät für Informatik
Chair IV, Software and Systems Engineering

Praktikum Beweiser im WS 2004/2005

Leitung:		Reinhold Letz	Tel. 289-17876	informatik.tu-muenchen.de

[ Praktikum Beweiser im Sommersemester 2004 ]

[ Praktikum Beweiser im Sommersemester 2005 ]

Aktuell

Die Klausur ist korrigiert: Resultate

Musterlösungen:

Klausur A Klausur B Die Scheine können ab 25.2.2005 bei Frau Müller (Raum 01.11.044) abgeholt werden.

Organisatorisches

Termine:	Vorlesung:	Mittwochs 14:15 - 15:45 Uhr
		Beginn: 27.10.2004
	Übung:	Mittwochs 13:15 - 14:00 Uhr (ab 3.11.2004)
Ort:	Garching	Informatik, Raum 00.13.009A
Sprechstunde:	Nach Vereinbarung	Garching, MI 00.09.065
Klausur:		Mittwoch, 9.2.2005, 15:15 - 16:45 Uhr
Ort:	München	Hörsaal N1179 (Wilhelm Nusselt-Hörsaal, Innenstadt Nordgelände, Zugang Theresienstr.)

Scheinabholung:		Sekretariat von Prof. Broy: Raum 01.11.044

Klausur im SS03
Klausur mit Lösungen im WS03/04
Klausur mit Lösungen im SS04

Inhalt

Während die Rolle der Logik als eine der wichtigsten Grundlagendisziplinen der Informatik schon immer unbestritten war, finden Verfahren der automatischen Deduktion zunehmend auch in der Praxis Anwendung, z.B. in den Bereichen Hardware- und Softwareverifikation, Programmentwicklung, Logikprogrammierung oder wissensbasierten Systemen.
Das Praktikum will in die Grundbegriffe der automatischen Deduktion einführen. Dazu werden im Vorlesungsstil die Grundlagen der Entwicklung automatischer Beweisverfahren fuer die Aussagenlogik und die Prädikatenlogik erarbeitet. In den Übungen werden dazu Aufgaben gerechnet, die auf die Klausur vorbereiten.

Voraussetzungen

Es sind keine speziellen Logikkenntnisse für die erfolgreiche Teilnahme am Praktikum erforderlich, da sämtliche theoretischen Grundlagen behandelt werden.

Praktikumsschein

Nach aktueller Prüfungsordnung: Gültig als Praktikumsschein für theoretische Informatik (Informatik III) ( Erläuterung dazu). Voraussetzung für den Schein sind regelmässige Teilnahme an der Vorlesung sowie ausreichende Leistungen in einer Klausur am Ende des Semesters. Die Scheine sind grundsätzlich benotet. Die Scheine sind im Sekretariat von Prof. Broy (Raum 01.11.044) abzuholen.