TU Wien Informatics

20 Years

Die Logik in der Informatik

  • 2014-05-27
  • Research

Logik und Informatik sind eng miteinander verwoben sind. Logik in der Informatik ist eines der Schwerpunktthemen beim “Vienna Summer of Logic 2014”.

TU Wien, Presseaussendung 2014, Florian Aigner

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.

Rückfragehinweis: Prof. Helmut Veith Institut für Informationssysteme Technische Unviersität Wien Favorigenstraß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

Links

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!