Alle Menschen sind sterblich. Sokrates ist ein Mensch. Also ist Sokrates sterblich. Solche logischen Schlussfolgerungen untersuchte man schon in der Antike. In den letzten Jahrzehnten hat sich die Logik-Forschung allerdings drastisch gewandelt: Die Computerwissenschaften wurden geboren. Ohne Vorarbeiten aus der Logik wäre die Entwicklung der Informatik nicht möglich gewesen – und umgekehrt liefert die Informatik bis heute laufend neue Fragestellungen, die nur mit Hilfe formaler Logik beantwortet werden können. Die Informatik ist daher nicht unbedingt als Tochter der Logik zu sehen – beide entwickeln sich wie Geschwister in enger Verbindung weiter.

Rechnen mit logischen Aussagen
Einfache logische Schlussfolgerungen, wie der berühmte aristotelische Syllogismus über die Sterblichkeit des Sokrates erscheinen uns unmittelbar einsichtig und einfach. Doch Logik erschöpft sich freilich nicht darin, das Offensichtliche zu formalisieren. Ebenso wie in der Mathematik lassen sich auch in der Logik beliebig komplexe Formeln aufstellen, mit denen man rechnen, argumentieren und die Welt analysieren kann.

Schon bevor die ersten elektronischen Rechenmaschinen gebaut wurden, machte man sich Gedanken über die Macht der Computer: Die Mathematiker Alan Turing und Alonzo Church untersuchten in den Dreißigerjahren, welche Klasse von Problemen überhaupt berechnet werden kann. Turing hatte sich ein Modell für eine ganz simple Rechenmaschine ausgedacht, die Turing-Maschine: An einem unendlich langen Band fährt eine Maschine entlang, liest Zahlen auf dem Band und kann sie nach vorgegebenen Regeln verändern.

Eine solche Maschine kann man aus Zahnrädern oder auch aus Lego bauen. Obwohl eine solche Maschine in der Praxis nicht effizient ist, kann man  zeigen, dass jede Computerberechnung im Grunde auch von einer solchen einfachen mechanischen Maschine durchgeführt werden könnte. Die Turing-Maschine erlaubte daher erstmals eine saubere Definition dessen, was „mathematisches Berechnen“ eigentlich bedeutet. Insbesondere konnte Turing damit auch zeigen, dass sich manche mathematische Fragen nicht durch Computer lösen lassen: So ist es etwa logisch nicht möglich, das ein Computerprogramm ein anderes Computerprogramm liest und entscheidet, ob dessen Berechnungen jemals an ein Ende gelangen oder unendlich lange weiterlaufen.

Blick nach innen, Blick nach außen
„Der größte Teil der Logik-Forschung wird heute in der Informatik betrieben, nicht in der Mathematik“, erklärt Prof. Helmut Veith vom Institut für Informationssysteme der TU Wien. Die Logik in der Informatik hat ganz unterschiedliche Aufgaben zu erfüllen: Zunächst ist sie, ganz ähnlich wie die Mathematik, ein Werkzeug, mit dem ein Computerprogramm die Welt beschreiben kann. So braucht man etwa Logik für moderne Datenbanken, oder um Computerprogrammen künstliche Intelligenz zu verleihen.

Doch die Logik ermöglicht einem Computer nicht nur den Blick auf die Welt, sondern auch nach innen: Computerprogramme können Computerprogramme überprüfen und auf logische Fehler untersuchen. „Das ist ähnlich wie beim Menschen“, meint Helmut Veith, „wir denken auch über die Welt um uns nach, wir können aber auch introspektiv über das Denken und über unser eigenes Gehirn nachgrübeln.“

Die logik-basierte Qualitätskontrolle  von Computerprogrammen (Verification, Model Checking) spielt heute eine sehr große Rolle für Industrie und Wirtschaft. Wenn man als Anwender ein Computerprogramm ausprobiert und alles funktioniert, bedeutet das noch lange nicht, dass das Computerprogramm fehlerfrei ist. Die Frage ist: Reagiert das Programm korrekt auf jeden nur denkbaren Input, in jeder logisch möglichen Situation? Das lässt sich nur von automatisierten Programmen überprüfen. Bei sicherheitsrelevanten Programmen – etwa der Steuerung eines Flugzeugs – ist ein solcher verlässlicher Check sehr wichtig. Auch in der Chipherstellung spielt das heute eine große Rolle: Chips entstehen zunächst als Computerprogramm, lange bevor sie tatsächlich gebaut werden. Kein Mensch könnte je per Hand analysieren, ob der Chip tatsächlich in jeder Situation das richtige Ergebnis liefert. Computerprogramme übernehmen diese logischen Tests heute und sorgen damit für unsere Sicherheit.


Die größte wissenschaftliche Veranstaltung in der Geschichte der Logik findet im Juli an der TU Wien statt. Für den „Vienna Summer of Logic“ wird Forschungsprominenz aus der ganzen Welt nach Wien kommen – in eine Stadt, die eng mit der Geschichte der Logik verknüpft ist.

Mehr über den Vienna Summer of Logic 2014 erfahren Sie hier: www.tuwien.ac.at/aktuelles/news_detail/article/8787/, öffnet eine externe URL in einem neuen Fenster

[1] Foto: Projet Rubens, ENS Lyon, Creative Commons
 
Rückfragehinweis:
Prof. Helmut Veith
Institut für Informationssysteme
Technische Universität Wien
Favoritenstraße 9-11, 1040 Wien
T: +43-1-58801-18441
helmut.veith@tuwien.ac.at

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