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

Praktikum Beweiser im SS 2005

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

[ Praktikum Beweiser im Wintersemester 2004/2005 ]

Aktuell

Die Scheine sind ab sofort bei Frau Müller (Raum 01.11.044) abholbar.

Resultate der Klausur vom 14.7.05

Resultate der Nachklausur vom 20.9.05

Bitte beachten Sie, dass das Praktikum Beweiser ab dem WS05/06 nicht mehr stattfindet. Bitte melden Sie sich bei einem anderen Praktikum aus dem Bereich Theoretische Informatik an (ab dem WS wird z.B. ein neues Praktikum "Analyse von Systemperformanz" angeboten.) Nach Prüfungsordnung können statt des Praktikums auch Leistungsnachweise aus Vorlesungen mit Übungen im Gesamtumfang von mindestens 6 Semesterwochenstunden vorgelegt werden. Die entsprechenden Vorlesungen dürfen dann bei den zur Diplomhauptprüfung anzugebenden Vorlesungen nicht noch einmal genannt werden.

Organisatorisches

Termine:	Vorlesung:	Donnerstags 15:05 - 16:35 Uhr

	Übung:	Donnerstags 12:05 - 12:50 Uhr
Ort:	Garching	Informatik, Raum 00.13.009A
Sprechstunde:	Nach Vereinbarung	Garching, MI 00.09.065
Klausur:		Donnerstag, 14.7.2005, 13:15 - 14:45 Uhr
Ort:	München	Hörsaal 1200 (Carl von Linde Hörsaal, Zentralgelände Innenstadt)

Es können in der Klausur alle Unterlagen verwendet werdet.

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

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.