| 
| 
| 
| 
| 
|
|
| 
| 
| ||
 |
 |
|
|
|
|
|
|
|
|
|
|
|
| ||
|
|
Viele Konzepte der Informatik haben ihre Wurzeln in der Logik. Zu den klassischen Anwendungsbereichen der Logik in der Informatik zählen der Hardwareentwurf, Komplexitäts- und Berechenbarkeitstheorie, Semantik von Programmiersprachen, Verifikation, Logikprogrammierung, Kuenstliche Intelligenz, wissensbasierte Systeme, Datenbanksysteme, u.v.m.
Beispielsweise basiert die Logiksynthese des Schaltkreisentwurfs auf aussagenlogischen Konzepten. Grundlegende Begriffe und Methoden gehen auf Boole (1847), Ehrenfest (1910) und Shannon (1938) zurueck. Die rasche Entwicklung der Informatik, die dazu fuehrte, dass heutzutage Prozessoren mit mehreren Millionen von Transistoren gebaut werden, macht maschinelle Entwurfsmethoden unerlässlich. Aus diesem Grund ist in den letzten Jahren sehr viel Bewegung in das Forschungsgebiet der Logiksynthese gekommen. Insbesondere erwähnenswert sind in diesem Kontext binäre Entscheidungsgraphen, die sich zur computerinternen Darstellung von Schaltfunktionen bewährt haben und die in den vergangenen 15 Jahren intensiv untersucht wurden.
Prädikatenlogische Konzepte (und Logiken höherer Ordnungen) spielen im Kontext von Programmiersprachen; insbesondere im Bereich der Semantik und der Verifikation eine wichtige Rolle. Beispielsweise basieren funktionale Programmiersprachen auf dem lambda-Kalkuel, während die Logikprogrammierung (z.B. PROLOG, DATALOG) auf Prädikatenlogik erster Ordnung beruhen. Fuer die Verifikation von Programmen hat sich die Hoare-Logik (und einige Varianten) etabliert. Diese stellt Vor- und Nachbedingungen für ein Programm durch prädikatenlogische Formeln dar und steht in engem Zusammenhang zu (denotationellen) Fixpunktsemantiken, die das Ein-/Ausgabeverhalten eines Programms beschreiben.
Temporale und modale Logiken haben sich als Spezifikationsformalismus fuer parallele reaktive Systeme etabliert. Im Gegensatz zum Einsatz zur Hoare-Logik, die das funktionale Ein-/Ausgabeverhalten eines (terminierenden) Programms formalisiert, können temporal- oder modallogische Formeln das unendliche Verhalten eines (fuer den Endlosbetrieb konzipierten) Computersystems beschreiben. Typische Beispiele fuer Eigenschaften, die durch temporale oder modale Logiken dargestellt werden können, sind "Jede Anfrage wird irgendwann beantwortet." oder "Niemals sind zwei Prozesse gleichzeitig in ihrem kritischen Abschnitt." Darueberhinaus gibt es zahlreiche Varianten temporaler und modaler Logiken, die es erlauben quantitative Aspekte (wie Zeit oder Wahrscheinlichkeiten) zu formalisieren. In den vergangenen 20 Jahren wurden für einige solcher temporalen und modalen Logiken sog. Model Checking Algorithmen entworfen und in Tools implementiert, die in zunehmenden Masse industrielle Anwendung finden. Model Checking Tools ermöglichen den vollautomatischen Nachweis, dass ein (Computer-)System temporal- oder modallogische Anforderungen erfuellt und unterstuetzen im Fehlerfall das Debugging durch die Ausgabe eines Fehlerhinweises.
Neben den vollautomatischen Analysemethoden gibt es deduktive Ansätze, die mit Hilfe eines Theorembeweisers in halbautomatischen Verfahren eingesetzt werden können. Deduktive Methoden sind neben der Programmverifikation auch in zahlreichen anderen Bereichen der Informatik bedeutsam. Beispielsweise beruht das Resolutionsprinzip, das grundlegend fuer Logikprogrammiersprachen wie PROLOG ist, auf einem Deduktionsprinzip.
Komplexitäts- und berechenbarkeitstheoretische Untersuchungen belegen die Grenzen von maschinellen Methoden. Neben den beruehmten Gödelschen Sätzen spielt hier z.B. der Satz von Cook (1971) eine wesentliche Rolle. Dieser dokumentiert die algorithmische Schwierigkeit aussagenlogischer Fragestellungen mit Hilfe des Begriffs der NP-Vollständigkeit. In diesem Kontext ist z.B. der Entwurf effizienter Algorithmen, die ein aus komplexitätstheoretischer Sicht "schwieriges" Problem approximativ lösen, ein wichtiges Forschungsgebiet.
Ferner weist das Gebiet "Formale Sprachen" (und verwandte Konzepte wie Grammtiken und Automatenmodelle) zahlreiche Bezüge zu Fragestellungen der Logik auf. Z.B. verwendet die übliche Definition des Berechenbarkeitsbegriffs das Modell von Turingmaschinen, deren Ausdrucksstärke auch durch Grammatiken vom Typ 0 charakterisiert werden kann. Ein weiteres Beispiel sind temporale Logiken, die in engem Zusamenhang zu sog. omega-Automaten stehen. Diese sind Erweiterungen von endlichen Automaten, die wiederum die Klasse des regulären Sprachen (Sprachen vom Typ 3) vertreten. Eine weitere Variante endlicher Automaten sind Mealy und Moore Maschinen, die für den Hardwareentwurf eine zentrale Rolle spielen.
Herr Karpinski interessiert sich für VC-Dimension und O-minimale Theorien.