Verifizierte Algorithmenanalyse

点击翻译按钮获取中文摘要

Beweisassistenten sind Programme zur Erstellung logisch 100% wasserdichter formaler mathematischer Beweise. Zwei herausragende Anwendungen von Beweisassistenten in den letzten 2 Jahre sind die Beweise des Satzes von Feit-Thompson (aus der Gruppentheorie) und der Keplerschen Vermutung (zur dichtesten Kugelpackung). Formale Beweise sind z.Z. noch sehr aufwändig, da die mathematischen Grundlagen vielfach noch nicht formalisiert wurden. Ziel dieses Projekts ist es, im Beweisassistenten Isabelle die notwendigen mathematischen Grundlagen für die quantitative Analyse von Algorithmen zu formalisieren und eine wiederverwendbare Bibliothek effizienter, determistischer und randomisierter Algorithmen bereit zu stellen, die sowohl in ihrer Funktionalität als auch in ihrer Effizienz verifiziert, d.h. korrekt bewiesen wurden. Als Grundlage sind Kombinatorik und Wahrscheinlichkeitstheorie zu formalisieren und mit einer Beweisumgebung für die Algorithmenanalyse und Verifikation zu verbinden. Zudem soll als Highlight Tuckers Beweis des 14. Problems von Smale (des Lorenz-Attraktors) verifiziert werden. Jenseits aller inhaltlichen Ziele möchte ich mit dem Projekt dazu beitragen, die meist disjunkte Forschung in den Bereichen Algorithmik und Logik zu verbinden um komplexe Ergebnisse der Algorithmik formalisieren zu können.