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

Praktikum Beweiser im SS 2004

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

[ Praktikum Beweiser im Wintersemester 2003/2004 ]
[ Praktikum Beweiser im Wintersemester 2004/2005 ]

Ausgeloste Teilnehmer am Praktikum im WS04/05

Aktuell
Die Scheine können in Raum 01.11.044 abgeholt werden.

Resultate der Klausur

Musterloesung A Musterloesung B

Eine Mitschrift der Veranstaltung wurde dankenswerterweise von Robert Rackl bereitgestellt: hier

Informationen zur Klausur

Es darf beliebiges Material verwendet werden.

Die wichtigsten speziellen Definitionen (z.B. Kalkülregeln) werden aber bei den Aufgaben jeweils noch angegeben.

Es werden keine Aufgaben zu Frege-Hilbert-Kalkülen (axiomatischen Kalkülen), zu Sequenzenkalkülen sowie zu prädikatenlogischen Tableaukalkülen gestellt.

Klausur im SS03 (keine Musterlösung vorhanden)
Klausur mit Lösungen im WS03/04
Lösungen der Aufgaben des SS03 (Aufgabenstellungen werden noch geliefert)

Organisatorisches

Termine:	Vorlesung:	Donnerstags 14:15 - 15:45 Uhr

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

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.