Master Thesis
Gilt »log 2x ≥ 2 log log x«? – Kern vieler Komplexitätsabschätzungen von Algorithmen sind mehr oder weniger schwierige algebraische Umformungen und Ungleichungen. In manchen Fällen sind solche Abschätzungen hinreichend komplex, dass ein computergestützer Beweis sehr wünschenswert wäre. Ziel dieses Projekts ist es, einen solchen auf traditionelle Art per Hand geführten Beweis mit Hilfe des Theorembeweisers Isabelle zu überprüfen. Das heißt, es sind die auf Papier vorliegenden Beweise in Isabelle zu formalisieren und so zu vervollständigen, dass das Isabelle-System jeden Umformungsschritt als korrekt akzeptiert.
Der konkrete Beweis, der hier formalisiert werden soll, findet sich in einer Arbeit über die Multiplikation eines Vektors mit einer dünn besetzten Matrix, wobei angenommen wird, dass bereits die Vektoren zu groß sind, um im Hauptspeicher Platz zu finden. Die zentrale Aussage ist eine untere Schranke für die Anzahl der Festplattenzugriffe. Dieser Beweis besteht aus drei Teilen: Zum einen das kombinatorische Argument, das zu einer Ungleichung führt (mit Potenzen von Binomialkoeffizienten), dann die Umformung der Ungleichung, und drittens die Abschätzungen, die ein Vereinfachen der Terme erlauben. Letztere Abschätzungen (wie z.B. die im Titel) stehen im Vordergrund des Projekts. Wenn möglich soll aber der gesamte Beweis formalisiert werden.
Isabelle ist ein System zur Formulierung und Überprüfung mathematischer Beweise. Der Bearbeiter dieses Projekts sollte entweder Isabelle schon kennen oder bereit sein, sich in das System einzuarbeiten. Diese Einarbeitung kann auch in Form eines Praktikums erfolgen bzw angerechnet werden.
Es werden gute Analysis-Kentnisse erwartet. Hilfreich, aber nicht notwendig, ist die Vorlesung Logik.
Betreut wird die Arbeit von Riko Jacob und Tobias Nipkow.