Verzeichnis eigener Lehrveranstaltungen

Grundstudium

Grundzüge der Informatik I: Programmierung
(V3/Ü2)
Objektorientierter Entwurf, Programmiersprachen, Verifikation (Anfängerveranstaltung mit Praktikum)

Grundzüge der Informatik IV: Einführung in die Theoretische Informatik
(V4/T1/Ü2)
Berechenbarkeit, Komplexität, Formale Sprachen

Orientierung über das Hauptstudium Informatik (V2)

Applied Logic:
(4 Credits)
Formale Logik, Beweiskalküle und ihre Anwendungen

Hauptstudium

Automatisierte Logik und Programmierung
(2 x V4/Ü2)
Zweisemestrige Einführung in die Grundlagen meines Forschungsgebietes, mit praktischen Übungen mit NuPRL.

Teil I: Formalisierung, Kalküle (intuitionistische Typentheorie) und interaktive Beweiser

Teil II: Implementierung von Beweissystemen, Automatisierung logischer Schlüsse, Synthese von Algorithmen

Programmsynthese / Konstruktion zuverlässiger Software
(V3/Ü2)
Einführung in Grundlagen und Methoden der rechnergestützten Softwareentwicklung

Inferenzmethoden
(V4/Ü2)
Einführung in Grundlagen und Methoden des automatischen Beweisens

Introduction to Automated Reasoning
(4 Credits)
Typentheorie, Beweissysteme und ihre Anwendungen

Computational Type Theory
(3 Credits)
Theoretische und semantische Grundlagen formaler konstruktiver Logiken

Grundlagen der Datenbanken (V3/Ü2)

Sozialorientierte Gestaltung von Informationstechnik
(V2/S2).
Interdisziplinäre Veranstaltung in Zusammenarbeit mit anderen Hochschullehrern der Informatik, der Soziologie,

der Sozialethik, der Arbeitspsychologie und dem Zentrum für interdisziplinäre Technikforschung.

Lehramtsstudium

Einführung in die Theoretische Informatik (V2/Ü2)

Einführung in die Künstliche Intelligenz (V2/Ü2)

Seminare

Die Entwicklung der Logik vom Altertum bis zur Gegenwart (S2)
Automatisches Planen (S2)
Programmsynthese und maschinelles Lernen (S2)
Typentheorie (S2)
Künstliche Intelligenz (S2)
Theorie der Berechenbarkeit (S2)
Kryptologie (S2)

Für die Zukunft geplante Lehrveranstaltungen

Logik, Kalküle und Beweisverfahren (V4/Ü2)

Rekursionstheorie (2 Semester, je V3/Ü2)

Komplexitätstheorie (V4/Ü2) 236

Doktoranden

Heiko Mantel:

Universität Saarbrücken, geplant für Mitte 2001.

Jens Otten:

Effiziente Beweisverfahren für konstruktive Logiken, TU Darmstadt, geplant für Mitte 2000.

Ozan Hafizogullari:

Extended Static Typechecking, Cornell-University, geplant für Mai 2000.

Stefan Schmitt:

Proof Reconstruction in Classical and Non-classical Logics, TU Darmstadt, November 1999.

Daniel Korn:

Konstruktiv adäquate Beweisautomatisierung für intuitionistische Logik, TU Darmstadt, November 1998.

Marion Kremer:

Entwurf eines sprachunabhängigen Verifikationssystems auf der Basis denotationaler Semantikbeschreibungen, TU Darmstadt, März 1996.

Diplomanden

Ferenc Kurucz:

Realisierung verschiedender Induktionsstrategien basierend auf dem Rippling-Kalkül, 1997.

Gerd Stolpmann:

Schematische Konstruktion von Globalsuchalgorithmen, 1997.

Oliver Hanemann:

Steuerung des NuPRL-Systems mit einer matrix-basierten Beweisstrategie, 1997.

Dirk Schlimm:

Intuitionismus und Informatik, 1997.
(Co-Betreuung mit Dr.Barbara Brüning, FB Philosophie)

Heiko Mantel:

Ein Matrix-Charakterisierung für ein Fragment der linearen Logik, 1996.

Tran van thanh Liem:

Induktion im NuPRL System, 1996.

Andreas Raab:

Prädikative Algorithmensynthese mit dem LOPS-Ansatz, 1996.

Eva Hornecker:

Grundzüge der Informatik I - Didaktische Analyse des Übungsbetriebes, 1995.
(Co-Betreuung mit Prof.Henhapl und Dr.Heger von der Hochschuldidaktischen Arbeitsstelle)

Jens Otten:

Ein konnektionen-orientiertes Beweisverfahren für intuitionistische Logik , 1995.

Stefan Schmitt:

Ein erweiterter intuitionistischer Sequenzenkalkül und dessen Anwendung im intuitionistischen Konnektionsbeweisen, 1995

Ilka Gassmann:

Eine Matrix-basierte Beweisprozedur für intuitionistische Top-Down Sequenzenbeweise, 1994.

Marco van den Berg:

Automatische Verifikation - ein unlösbares Problem?, 1994.

Stefanos Padelis:

Steuerung von Programmsynthesen mit dem LOPS-Ansatz, 1994.

Daniel Korn:

KonSequenz - Ein Konnektionsmethoden-gesteuertes Sequenzenbeweis-Verfahren, 1993.

Martina Hammel:

Hypothesenanalyse von Künstlicher Intelligenz und Konnektionismus: Zu den Wechselwirkungen zwischen Wissenschaft und Gesellschaft, 1991.

Didaktische Schulungen

Ich habe an mehreren Schulungen der hochschuldidaktischen Arbeitsstelle der TU Darmstadt teilgenommen und seit 1994 an der Gestaltung neuer Schulungen mitgewirkt. Themen waren:

-

Didaktik der Lehre in Vorlesung, Seminar und Übung

-

Rhetorik von Vorträgen,

-

Diskussionsverhalten und Teamarbeit,

-

Betreuung von Examensarbeiten,

-

Schulung von Tutoren für Übungsgruppen,

-

Gestaltung und Betreuung von Promotionsvorhaben.

-

Prüfungen: Formen und Gestaltung.

Referenzen

Eine inhaltliche Einschätzung meiner Forschungsarbeiten können abgeben

• Prof.R.Constable, Department of Computer Science, Cornell University, Ithaca, USA
  e-mail: rc@cs.cornell.edu

• Prof.W.Bibel, FG Intellektik - FB Informatik, TU Darmstadt,
  e-mail: bibel@intellektik.informatik.tu-darmstadt.de

• Prof.H.Schwichtenberg, Mathematisches Institut der Universität München
  e-mail: schwicht@rz.mathematik.uni-muenchen.de

• Prof.F.Pfenning, Dept.of Computer Science, Carnegie Mellon University, Pittsburgh, USA
  e-mail: fp@cs.cmu.edu

• Prof.F.von Henke, Abtl. Künstliche Intelligenz, Universität Ulm
  email: vhenke@ki.informatik.uni-ulm.de

• Prof.K.Weihrauch, FB Mathematik und Informatik, FernUniversität Hagen  (frühe Arbeiten)
  e-mail: klaus.weihrauch@fernuni-hagen.de

Eine Beurteilung meiner Lehrtätigkeit an der TU Darmstadt können abgeben

• Prof.W.Henhapl, FB Informatik, TU Darmstadt
• Prof.W.Bibel, FB Informatik, TU Darmstadt
• Dr.Michael Heger, Hochschuldidaktische Arbeitsstelle der TU Darmstadt (jetzt FH Aachen)

Ithaca, 10. April 2000