Proseminar: Mathematische und logische Perlen der Informatik
Fakultät für Informatik

TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

TUM

Proseminar | Sommersemester 2005
Mathematische und logische Perlen der Informatik
Tobias Nipkow, Amine Chaieb

 

(Mittwochs 14-16 Uhr, Raum MI 00.11.038)


Zusammenfassung

Es gibt viele interessante Themen in der Informatik, die im Studium gar nicht, nur unzureichend, oder erst gegen Ende behandelt werden, die aber sowohl wegen ihrer Relevanz als auch wegen der Schönheit der Lösung zu den Perlen zählen. Dieses Proseminar möchte Sie gerne mit einigen davon bekannt machen. Der Schwerpunkt liegt dabei auf Problemen an der Schnittstelle von Informatik, Mathematik und Logik.

Themenliste:


  1. Kildalls Algorithmus wird in der Programmanalyse eingesetzt. Er führt das Herausfinden bestimmter Programmeigenschaften auf die iterative Lösung eines Ungleichungssystems zurück. Im Vordergrund steht die Arbeitsweise und die Korrektheit dieses Algorithmus.
  2. Coxeter-Todd: Ein einfacher aber effektiver Algorithmus aus der Gruppentheorie, der die Anzahl der Nebenklassen ein Gruppe bestimmt
  3. Graphenfärbung: wird eingesetzt sobald eine Verteilung von mehrern Objekten auf eine kleinere Menge stattfinden soll, wobei die Objekte von einander abhängen können (z.B. in Compilern - Registervergabe).
  4. Lambda Kalkül ist ein minimales Kalkül, das den Kern aller funktionalen Programmiersprachen modelliert. Auf der Basis von nur 3 Konstrukten und einer Rechenregel kann man Boolesche Werte, Zahlen, Listen und eine ganze Programmiersprache schaffen.
  5. Typisiertes Lambda Kalkül: Haben Sie sich schon mal gefragt, wie in funktionalen Sprachen der Typ einer Funktion automatisch berechnet werden kann? Die Antwort darauf kann man am besten am typisierten Lambda Kalkül erklären.
  6. Unifikation: Wer sich mal gefragt hat, wie Pattern Matching in funktionalen und insbesondere in logischen Programmiersprachen (wie Prolog, Gofer, ML, Haskell etc) funktioniert wird hier eine Anwort finden.
  7. Resolution : ist ein mächtiges Verfahren um zu entscheiden ob eine (hier aussagenlogische) Formel wahr oder falsch ist.
  8. Davis Putnam: ist ein weit verbreitetes und schnelleres Verfahren, um das obige Problem zu entscheiden.
  9. Rabin-Miller Primatitätstest ist ein faszinierend einfacher und sehr relevanter probabilistischer Primalitätstest. Wird die Zahl nicht akzeptiert, so ist sie mit Sicherheit keine Primzahl. Akzeptiert das Verfahren die Zahl, so bedeutet das, dass sie mit sehr hoher Wahrscheinlichkeit eine Primzahl ist.
  10. Symbolische Berechnung mit Summen: Wie kann man geschachtelte Summenausdrülcke vom Computer berechnen lassen? Sowohl Computeralgebrasysteme als auch Theorembeweiser verfügen ülber solche Möglichkeiten. Hier wird ein "einfacher" Fall behandelt.
  11. Simplex: Das Simplex-Verfahren ist ein Algorithmus zur Optimierung linearer Programme. Ein lineares Programm besteht aus einer zu maximierenden bzw. minimierenden linearen Funktion f, und einer endlichen Menge linearer Ungleichungen, die den Definitionsbereich von f einschränken. Es wird eine Darstellung der Theorie des Verfahrens erwartet (also warum das Verfahren überhaupt funktioniert). Literatur in diesem Bereich ist häufig in englischer Sprache verfasst, deshalb sollten diesbezüglich keine Berührungsängste bestehen.

Lernziele

  • Selbständige Einarbeitung in wissenschaftliche Literatur.
  • Präsentationstechniken.
  • Umgang mit LaTeX, einem System zum Schreiben technischer Texte.
  • Programmierung kompakter mathematischer/logischer Algorithmen.

Anmeldung



* Interessentinnen/en können sich bei der Vorbesprechung oder vorab per Email bei chaieb "at" in.tum.de anmelden. In der E-Mail sollen folgende Informationen enthalten sein: 
  • Name, Vorname
  • Studiengang und Studienfach
  • Semester
  • E-Mail (nur Adressen @in.tum.de)
  • bevorzugtes Thema

Vorbesprechung



* Die Vorbesprechung findet am Mo. 07.02.2005,  14.00 Uhr im Raum MI 00.09.055 statt.

Termine und Betreuer

Das Proseminar findet Mittwochs von 14 Uhr bis 16 Uhr im Raum 00.11.038 statt.
Termin
Thema
Bearbeiter
27.04
Resolution
Manfred Pauli
27.04
Davis Putnam
Sun Haifeng
04.05
Unifikation
Shan Du
11.05
Kildall
Rumpel
25.05
Lambda Kalkuel
Irune Erodicia Diaz
01.06
Summen
Cong Manh Tran



Hinweise

Ein Schein wird für folgende Leistungen vergeben : eine in LaTeX geschriebene Ausarbeitung, ein Vortrag, eine Implementierung (wenn verlangt) und die regelmässige Anwesenheit.

Hinweise zur Anfertigung einer Seminararbeit



* Die Seminararbeiten sollten mit dem Textsatzsystem LaTeX erstellt werden.
* Bei Fragen zu LaTeX sei einerseits auf die folgenden Links hingewiesen, ferner kann auch der Betreuer um Hilfestellungen bzw. Literaturangaben gebeten werden:

* Eine weitere Anleitung zur Erstellung von Ausarbeitungen finden sie hier.
* Informationen zur Installation von LaTeX unter Windows finden Sie hier.

Hinweise zur Gestaltung der Vorträge



* Wer seine Folien mit LaTeX erstellen möchte findet hier einige Hinweise (einschließlich Rahmen-Datei als Vorlage)

© Software & Systems Engineering Research Group
Sitemap |  Kontakt/Impressum
Letzte Änderung: 2005-04-19 18:39:37