Skip to main content
Zur Startseite der DHBW Stuttgart 50 Jahre DHBW Stuttgart 50 Jahre DHBW Stuttgart
Standorte
Stuttgart Campus Horb
DE  |  EN
Studieninteressierte Studierende Duale Partner Lehrbeauftragte Presse Alumni International Visitors Mitarbeitende
Zur Startseite der DHBW Stuttgart

Erneuter Erfolg bei Weltmeisterschaft für automatische Beweiser

In der CADE ATP System Competition, der Weltmeisterschaft für automatische Beweiser, besteht die SLH-Division (Sledgehammer-Division) aus Beweisaufgaben, die menschliche Nutzer*innen mit dem interaktiven Beweiser „Isabelle“ beweisen wollen und die in eine für automatische Beweiser geeignete Logik übersetzt wurden. In dieser Division hat der an der DHBW Stuttgart entwickelte Theorembeweiser „E“ den Wettbewerb im Rahmen der FLoC Olympic Games in Haifa (Israel) gewonnen.

Der an der DHBW Stuttgart entwickelte Theorembeweiser E feiert Erfolge bei FloC Olympic Games in Haifa (Israel)

Prof. Dr. Stephan Schulz trat mit „E“ in sechs der insgesamt sieben Divisionen an und erzielte neben dem ersten Platz in SLH auch drei zweite Plätze in den Divisionen FOF (klassische Prädikatenlogik erster Stufe, die "Königsdisziplin"), UEQ (unbedingte Gleichheitslogik) und THF (Prädikatenlogik höherer Stufe). Einen dritten Platz gab es in der Division LTB (Beweisaufgaben mit sehr großen Axiomenmengen in verschiedenen Codierungen).

 „If all you have is a hammer, every problem looks like a nail – wenn du nur einen Hammer hast, sieht jedes Problem aus wie ein Nagel “ war wohl die Inspiration, die Lawrence Paulson an der Universität Cambridge dazu bewegte, automatische Theorembeweiser als Back-End für den interaktiven Beweiser „Isabelle“ einzusetzen und diesen Ansatz Sledgehammer (=Vorschlaghammer) zu nennen.

Theorembeweiser sind Computerprogramme, mit denen man formal nachweist, dass bestimmte Aussagen zwingend aus einer gegebenen Beschreibung folgern. Beispiele im Kleinen wären z. B. die Beweise, dass ein Computerprogramm immer innerhalb einer bestimmten Zeit reagiert (und etwa die Bremse eines autonomen Fahrzeuges betätigt), oder dass eine Banktransaktion immer entweder vollständig oder gar nicht abgewickelt wird. Im Großen kann inzwischen die funktionale Korrektheit von komplexen Programmen wie z. B. einem Betriebssystemkern nachgewiesen werden und es gibt Projekte, in denen große Teile der klassischen Mathematik noch einmal formal nachgebildet werden.

Interaktive Beweiser wie „Isabelle“ unterstützen typischerweise Prädikatenlogik höherer Stufe und damit einen sehr mächtigen Formalismus. Sie verlassen sich aber darauf, dass ein Benutzer bzw. eine Benutzerin den Beweisvorgang steuert und fast alle wichtigen Entscheidungen über anzuwendende Taktiken selbst trifft - z. B. Fallunterscheidung, Induktion oder Beweis durch Widerspruch. Automatische Beweiser dagegen setzen in der Regel auf die Prädikatenlogik erster Stufe, bieten dafür aber hohe Geschwindigkeit, vollständige Kalküle und eine vollautomatische Beweissuche. Sledgehammer, das von Paulson erdachte und inzwischen mit vielen anderen Wissenschaftlern weiterentwickelte Werkzeug, wandelt Teilaufgaben des interaktiven Beweisers automatisch in geeignete Probleme für vollautomatische Beweiser um und entlastet damit die Nutzer*innen solcher Systeme ganz erheblich.

Weiterführende Links: