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

Automatischer Beweiser E verteidigt ersten Platz

Bei der CADE ATP System Competition, der Weltmeisterschaft für automatische Deduktionssysteme, war der Beweiser E der DHBW Stuttgart erneut erfolgreich. Der Wettbewerb fand im Rahmen der International Conference on Automated Deduction (CADE) in Rom statt.

Übergabe des Siegerpokals an Prof. Dr. Stephan Schulz durch den Organisator Dr. Geoff Sutcliffe

Der Beweiser E, primär von Prof. Dr. Stephan Schulz, Studiengangsleiter Informatik an der DHBW Stuttgart, entwickelt, konnte dabei seinen Erfolg aus dem Jahr 2022 wiederholen und erneut die Kategorie SLH (Sledgehammer) gewinnen.

Die Beweiser bekommen pro Kategorie eine Anzahl von Beweisproblemen, in der Regel bestehend aus einer Menge von Axiomen und einem zu beweisenden Theorem. Sie versuchen dann, innerhalb eines gegebenen Zeitlimits automatisch einen mathematisch schlüssigen Beweis für das Theorem zu konstruieren. In der Kategorie SLH kommen die Probleme aus dem Tool Sledgehammer, ursprünglich von Larry Paulson von der Universität Cambridge entwickelt. Sledgehammer unterstützt Nutzer des interaktiven Beweisers Isabelle z. B. bei der Entwicklung von mathematischen Systemen oder der Verifikation von Software. E löste in dieser Kategorie 467 von 1000 Problemen, die beiden stärksten Konkurrenten, der Beweiser Vampire von der Universität Manchester und der TU Wien sowie das System CVC5 von der University of Iowa, kamen auf 454 bzw. 362 Lösungen.

Neben dem Sieg in der Kategorie SLH konnte E den zweiten Platz in der Kategorie FOF (Probleme in der Prädikatenlogik erster Stufe) erkämpfen, die oft als Königsdisziplin angesehen wird. Zwei dritte Plätze in UEQ (unbedingte Gleichheitsbeweise) und THF (Prädikatenlogik höherer Stufe) runden den Erfolg ab.

In diesem Jahr fand die CADE gemeinsam mit der Conference on Formal Systems for Computation and Deduction (FSCD) an der Universität La Sapienza in Rom statt. Als Teil der Konferenz wurde auch wieder die CADE ATP System Competition ausgetragen.