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

Großer Erfolg bei der „World Championship for Automated Deduction“

Der Theorembeweiser E der DHBW Stuttgart hat auf dem Wettbewerb der Conference on Automated Deduction (CADE) in Natal/Brasilien, der „Weltmeisterschaft für Computerbeweiser“, einen ersten und zwei zweite Plätze erreicht.

Preisverleihung an Prof. Dr. Stephan Schulz, DHBW Stuttgart, durch Prof. Dr. Geoff Sutcliffe, University of Miami (v.r.n.l.)

Automatische Theorembeweiser sind Computerprogramme, die mit mathematischer Genauigkeit beweisen, dass eine Vermutung zwingend 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.

Die CADE veranstaltet seit 1996 jährlich die CADE ATP System Competition, um die Leistungen von Beweisern zu vergleichen. Dabei versuchen die Systeme in verschiedenen Kategorien möglichst viele Aufgaben zu lösen.

Der an der DHBW Stuttgart entwickelte Beweiser E gewann in der Kategorie UEQ den ersten Platz. In der Königsklasse (Formeln der Prädikatenlogik erster Stufe) erreichte E nach dem Beweiser Vampire der University of Manchester den zweiten Platz. Ebenfalls für den zweiten Platz reichte es in der Kategorie LTB. Neben den direkten Erfolgen war E auch indirekt an den Systemen Satallax und LEO-III, den Siegern zweier Kategorien beteiligt, indem diese E verwendeten, um Teilprobleme zu lösen.