Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage mit logischen Kalkülen dem Resolutionssystem und anderen Formen des automatischen Beweisens, regulären und kontextfreien Sprachen, endlichen Automaten und Turingmaschinen sowie Aspekten der Komplexitätstheorie umzugehen.
Die Vorlesung beginnt mit einer Einführung in die Theorie endlicher Automaten
und formaler Sprachen. Wir lernen die Klassen der regulären und der
kontextfreien Sprachen kennen, sowie verschiedene Beschreibungsformalismen für
derartige Sprachen, insbesondere endliche Automaten und formale Grammatiken.
Im zweiten Teil, nach einem starken Sprung in der Ausdrucksstärke, beschäftigen
wir uns mit Berechenbarkeitstheorie, d.h. mit der Frage welche Funktionen
überhaupt prinzipiell berechenbar sind. Dazu verwenden wir die
Operatordarstellung partiell rekursiver Funktionen sowie Turingmaschinen. Wir
diskutieren die Church-Turing-These und beweisen die grundlegenden Resultate
der Berechenbarkeitstheorie. Im dritten Teil behandeln wir die
Komplexitätstheorie. Diese erhält man aus der Berechenbarkeitstheorie durch eine
Einschränkung der für eine Berechnung zur Verfügung stehenden Resourcen, z.B.
auf polynomiale Zeit. In dieses Gebiet fällt das P vs. NP - Problem das wir ins
Zentrum unserer Diskussion der Komplexitätstheorie stellen werden. In einem
vierten Teil beschäftigen wir uns abschließend noch mit den theoretischen
Grundlagen der Programmverifikation, was die Anwendung und Zusammenführung
einer Reihe von Resultaten aus den vorherigen Teilen erlaubt.
