Alles logisch?

Ein Workshop für SchülerInnen im Rahmen der TEC-Initiative

Logik spielt eine bedeutende Rolle in vielen Wissenschaftsfeldern. Zum Beispiel wird sie in der Philosophie verwendet, um allgemeine Theorie zum korrekten Schließen und Argumentieren aufzustellen. In der Mathematik wird Logik verwendet, um Beweise zu führen und in der Elektrotechnik können Schaltkreise mit logischen Formeln beschrieben werden.

Auch in der Informatik findet Logik viele Anwendungen. Hier wird sie verwendet, um unterschiedlichste Probleme automatisch zu lösen. Aufgaben wie die Erstellung von optimalen Stundenplänen oder das Finden der kürzesten Route zwischen 2 Städten können einfach in die Sprache der Logik übersetzt werden und für das Lösen an hoch-optimierte Programme, sogenannte automatische Beweiser, übergeben werden. Hierbei werden die Inferenzmechanismen der Logik ausgenutzt, um aus bekannten Fakten neues Wissen abzuleiten. Logik dient so als Sprache, die verwendet wird, um Probleme in einer Form zu beschreiben, die von den automatischen Beweisern verstanden wird. Hat man eine Übersetzung eines Problems in die Sprache der Logik gefunden, kann der Computer das Problem lösen, ohne dass ein spezielles Programm erstellt werden musste.

In diesem Workshop untersuchen wir, wie uns automatische Beweiser helfen können, Rätsel wie Sudoku völlig automatisch zu lösen. Anhand dieser einfachen Spiele lernen wir die Grundkonzepte logischer Sprachen kennen und betrachten auf welche Weise moderne automatische Beweiser Probleme lösen.

Voraussetzungen: Keine.

Dauer: Ein Nachmittag (ca. 3h, mit Pausen)

Teilnehmerzahl: max. 25

Workshopleiter und Kontaktperson: Univ.-Prof. Dr. Armin Biere, Assoc.-Prof. Dr. Martina Seidl, Institut für Formale Modelle und Verifikation