Aktuelles Informatik

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

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

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. 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.