Informatik, TU Wien

Die ersten Olympischen Spiele der Logik

Die TU Wien ist der erste Austragungsort der Olympischen Spiele der Logik: Teams aus der ganzen Welt entwickelten Computerprogramme, die nun beim „Vienna Summer of Logic“ gegeneinander antreten.

TU Wien, Presseaussendung 71 / 2014, Florian Aigner

Muskelkraft wird bei den olympischen Spielen der Logik nicht gefragt sein. Stattdessen kommt es auf Schnelligkeit, Anpassungsfähigkeit und Intelligenz an, wenn Computerprogramme, entwickelt von Forschungsteams aus der ganzen Welt, bei Logik-Wettbewerben gegeneinander antreten. Die olympischen Spiele sind Teil des „Vienna Summer of Logic“, der größten wissenschaftlichen Veranstaltung in der Geschichte der Logik. Für Informatik-Interessierte gibt es kommentierte Liveübertragungen auf „Big Screens“ an der TU Wien, die Preisverleihungs-Zeremonien finden am 17. und am 21. Juli statt.

Von nun an im Vier-Jahres-Takt

„Citius, Maius, Potentius – schneller, größer, mächtiger“, so lautet das Motto der olympischen Spiele der Logik. „Wettbewerbe, bei denen Teams unterschiedlicher Universitäten Programmcodes gegeneinander antreten ließen, gab es bereits“, sagt Hauptorganisator Thomas Krennwallner (Institut für Informationssysteme, TU Wien). „Nun allerdings werden sie anlässlich des Vienna Summer of Logic zu einer einzigen Wettbewerbs-Großveranstaltung verschmolzen.“

Damit wird eine neue Tradition begründet: Wie die sportlichen olympischen Spiele sollen die „FLoC Olympic Games“ („FLoC“ steht für „Federated Logic Conference“) von nun an alle vier Jahre stattfinden. Wie es sich für olympische Spiele gehört, werden auch Medaillen vergeben. Ihre Vorderseite ziert ein Portrait des großen Wiener Logikers Kurt Gödel.

Bei den meisten Wettbewerben ist ein menschliches Eingreifen nicht erlaubt. Die Computerprogramme wurden – meist in Gemeinschaftsarbeit von mehreren Personen – bereits fertig vorbereitet, nun müssen sie gegeneinander antreten und in gegebener Zeit möglichst viele Logik-Probleme lösen. Je nach Disziplin können das ganz unterschiedliche Aufgaben sein, etwa das Auffinden von logischen Fehlern in Computerchips, das automatische Analysieren von Programmcode oder das Erstellen von mathematischen Beweisen.

Mitfiebern vor den „Big Screens“

„Jene Wettbewerbe, die eine sehr lange Rechenzeit benötigen, haben bereits begonnen, viele finden dann auch während des Vienna Summer of Logic zwischen 13. Juli und 21. Juli statt“, erklärt Thomas Krennwallner. Bei Fußball-Weltmeisterschaften gibt es Fanmeilen und Public Viewings , bei den Olympischen Spielen der Logik gibt es „Big Screens“ an der TU Wien (im großen Hörsaal in der Gusshausstraße und im Freihaus in der Wiener Hauptstraße).

Informatikinteressierte Zuseher können dort live den Stand der aktuellen Wettbewerbe mitverfolgen, sich Details erklären lassen und mitfiebern. Ausgiebig gejubelt wird dann sicher bei den beiden Preisverleihungs-Zeremonien. Sie finden am 17. Juli und am 21. Juli, jeweils von 16:30 bis 19:00 statt.
„Für uns sind die Olympischen Spiele der Logik viel mehr als bloß eine unterhaltsame Spielerei“, sagt Thomas Krennwallner. „Für die Forschung ist es wichtig, Theorie und Praxis zu verknüpfen. Um bei diesen Wettbewerben zu gewinnen, muss man komplizierte theoretische Konzepte auf praxisnahe Aufgaben anwenden, wie sie auch in der Computerindustrie jeden Tag gelöst werden müssen.“ Umgekehrt liefern die Probleme aus der Praxis wichtige Ideen für die theoretische Forschung.

Logik und Olympia – eine logische Kombination

So wie die olympischen Spiele auf die antike Tradition zurückverweisen baut auch die Logik-Forschung auf Fundamenten der griechischen Antike auf. Aristoteles beschäftigte sich ausführlich mit Logik, im zwanzigsten Jahrhundert wurde die formale Logik dann zu einem wichtigen Instrument für die Mathematik, heute sind die Methoden der Logik aus der modernen Informatik nicht mehr wegzudenken.

Big Screens

  • Freitag, 18. Juli 2014, 09:00-18:00: OWL Reasoner Evaluation (ORE) im Neuen EI Gebäude, Gusshausstraße 25-29, Foyer vor dem EI 7 Hörsaal
  • Freitag, 18. Juli 2014, 09:00-18:00: Satisfiability Modulo Theories solver competition (SMT-COMP) im Freihaus, Wiedner Hauptstraße 8-10, Foyer 2. Stock, vor dem FH HS1 Hörsaal
  • Sonntag, 20. Juli 2014, 10:00-18:00: Automatic Theorem Proving Competition (CASC) und Termination Competition (termComp) im Freihaus, Wiedner Hauptstraße 8-10, Foyer 2. Stock, vor dem FH HS1 Hörsaal
  • Sonntag, 20. Juli 2014, 14:30-16:00: Answer Set Programming Modeling Competition im Freihaus, Wiedner Hauptstraße 8-10, im FH HS2 Hörsaal

Zeremonien

  • Donnerstag, 17. Juli 2014, 16:30-19:00: FLoC Olympic Games Award Ceremony 1 für Confluence Competition (CoCo 2014), Configurable SAT Solver Challenge (CSSC 2014), Max-SAT Evaluation (Max-SAT 2014), QBF Gallery 2014, und SAT Competition 2014.
  • Montag, 21. Juli 2014, 16:30-19:00: FLoC Olympic Games Award Ceremony 2 für Answer Set Programming Competition (ASPCOMP 2014), IJCAR ATP System Competition (CASC-J7), Hardware Model Checking Competition (HWMCC 2014), OWL Reasoner Evaluation (ORE 2014), Satisfiability Modulo Theories solver competition (SMT-COMP 2014), Competition on Software Verification (SV-COMP 2014), Syntax-Guided Synthesis Competition (SyGuS-COMP 2014), Synthesis Competition (SYNTCOMP 2014), Termination Competition (termCOMP 2014).

Die Wettbewerbsdisziplinen der Logik

Die Olympischen Spiele der Logik setzen sich aus 14 Disziplinen zusammen, die in verschiedene „klassische logische Sportarten“ eingeteilt werden können.

Verifikation von Hardware und Software

Kann man sich darauf verlassen, dass ein bestimmter Computerchip immer die richtigen Rechenergebnisse liefert, oder dass ein bestimmtes Programm niemals abstürzt, egal welche Eingabedaten es bekommt? Computercodes können mit logischen Methoden Hard- und Software überprüfen. Besonders wichtig ist das für die Computerchip-Industrie, aber auch für Bereiche, in denen Programmfehler katastrophale Folgen hätten – etwa bei den Programmcodes einer Raumstation.

Software-Synthese

Warum soll nicht auch das Programmieren selbst von Programmen übernommen werden? Nach vorgegebenen Regeln müssen Computerprogramme in dieser Disziplin eigenständig Codes generieren.

Das Halteproblem

Kommt ein bestimmtes Computerprogramm bei seiner Rechnung je an ein Ende, oder verfängt es sich in einer unendlichen Schleife? Rigoros lässt sich diese Frage so allgemein nicht beantworten, wie der Computerpionier Alan Turing bewies. Aber kluge Programmcodes kommen bei solchen Analysen anderer Programme trotzdem meist zu einem Ergebnis.
Automatisches Beweisen
Lässt sich eine bestimmte logische Aussage aus anderen logischen Aussagen ableiten? Computerprogramme können heute selbstständig Beweise führen und klären, ob eine Aussage in einem bestimmten logischen Zusammenhang bewiesen werden kann.

Intelligentes Datenmanagement

Eine Liste der Straßen und Geschäfte einer Stadt zu erstellen, ist nicht schwer. Aber wie kann man effizient nach Daten suchen, um intelligente Suchanfragen beantworten zu können – zum Beispiel nach einem Park in der Nähe von einem Kino, bei einer Cocktailbar? Kompliziertes Datenbankmanagement benötigt heute die Methoden der Logik.

Planen, Analysieren, Probleme Lösen

Mehrere Wettbewerbe haben mit künstlicher Intelligenz zu tun. Hier geht es um Aufgaben, die vom Computer nicht durch bloßes numerisches Ausrechnen oder durch Durchprobieren einer großen Anzahl möglicher Lösungen erfüllt werden können. Für viele schwierige Rechenprobleme braucht das Computerprogramm ein intelligentes Problemlösungskonzept, zum Beispiel wenn die kürzeste Route gefunden werden soll, die viele vorgegebene Etappenziele in beliebiger Reihenfolge miteinander verbindet, oder für die Koordination von Flugzeugen und Startbahnen auf einem vielbenutzten Flughafen.

 

Aussender:
Dr. Florian Aigner
Büro für Öffentlichkeitsarbeit
Technische Universität Wien
Operngasse 11, 1040 Wien
T: +43-1-58801-41027
florian.aigner@tuwien.ac.at