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 Computerbeweiser“

Die DHBW Stuttgart konnte mit dem Theorembeweiser E international erneut Erfolge feiern: E erreichte auf der von der Conference on Automated Deduction (CADE) veranstalteten 25. CADE ATP System Competition, der „Weltmeisterschaft für Computerbeweiser“, zwei erste Plätze.

Die im Dunkeln leuchtende Siegertrophäe ging an den Theorembeweiser E der DHBW Stuttgart Bildquelle: Geoff Sutcliffe, University of Miami, FL

Der Theorembeweiser E wurde von Prof. Dr. Stephan Schulz im Studiengang Informatik der DHBW Stuttgart entwickelt. Automatische Theorembeweiser sind Computerprogramme, die mit zwingender Logik beweisen, dass eine Vermutung aus einer Menge von Axiomen folgt. Axiome und Vermutung sind dabei Formeln, z. B. der Prädikatenlogik erster Stufe. Die Formeln werden logisch kombiniert, um daraus neue Fakten abzuleiten. Die Anzahl der möglichen Ableitungen ist enorm groß und nur wenige führen zum Ziel. Theorembeweiser müssen möglichst schnell kombinieren, aber ebenso entscheiden, welche der vielen möglichen Ableitungen sie verfolgen. Damit sind sie sowohl ein Werkzeug als auch ein Gegenstand der Künstlichen Intelligenz.

Der Stuttgarter Beweiser E konnte in der Kategorie UEQ seinen ersten Platz des letzten Jahres verteidigen. In der Königsklasse, Formeln der Prädikatenlogik erster Stufe, gewann wieder der Beweiser „Vampire“ der University of Manchester. Auf dem zweiten Platz landete „Enigma“, eine Kooperation des Beweisers E mit einem maschinellen Lerner der Charles Technical University in Prag. Den dritten Platz erreichte E alleine. Für einen weiteren ersten Platz reichte es in der Kategorie LTB, in der über zwei Tage 10.000 Probleme in jeweils acht verschiedenen Formalisierungen zu beweisen waren.

Seit 1996 wird jährlich die CADE ATP System Competition abgehalten, um die Leistungen von Beweisern zu vergleichen. Dieses Jahr fand der Wettbewerb im Rahmen der International Joint Conference on Automated Reasoning (IJCAR) statt, die wegen der Corona-Epidemie zwar in Paris geplant war, dann aber weltweit online durchgeführt wurde.

Weitere Informationen zum Theorembeweiser E: https://www.eprover.org