Logik-Kalküle

40 Präsenzstunden Vorlesung, 20 Präsenzstunden Übung, 35 Stunden Vor-/Nachbereitung der Übungen, 55 Stunden Nachbereitung der Vorlesung und Prüfungsvorbereitung

Keine

Fähigkeit, Methoden der mathematischen Logik zur Modellierung syntaktischer und semantischer Aspekte von Problemstellungen, vorwiegend aus dem Bereich der Informatik, einzusetzen. Fundierte Kenntnisse über die Stärken und Schwächen, sowie die prinzipiellen Grenzen, der formalen Methode.

Die Vorlesung führt ein in Begriffe und Methoden der mathematischen Logik. Der Schwerpunkt der Vorlesung liegt auf den vielfältigen Anwendungen der Logik in der Informatik. Nach einer Einführung in die grundlegenden Begriffe Syntax, Semantik, Interpretation und Modell, schliesst sich eine eingehende Untersuchung des Beweisbegiffs, als semantisch korrekte, syntaktische Transformation an. Als wichtiges Beispiel wird der Kalkül des natürlichen Schliessens (nach Gentzen) eingeführt. Die Korrektheit der Minimallogik und die Vollständigkeit der klassischen Logik (nach Beth, Hintikka und Schütte) wird exemplarisch bewiesen. Es schliesst sich eine Erörterung des Lambda-Kalküls und der Curry-Howard-Korrespondenz an. Es folgen Ergebnisse zur Metamathematik(Gödel, Turing, Church, Loewenheim-Skolem). Weiter werden verschiedene einfache Logik-Kalküle vorgestellt und auf ihre wichtigsten Eigenschaften, Korrektheit und (Un-)Vollständigkeit, untersucht. Dazu gehören insbesondere beschränkt quantifizierte Formeln und Herbrand Modelle mit ihren Anwendungen auf die Formalisierung von Datenbanken, sowie Hornklauseln und SLD-Resolution mit ihren Anwendungen in der Logikprogrammierung.

Tafel, Folien, Beamer, Theorembeweiser (Minlog, MPC)

• Schöning: Logik für Informatiker, BI-Wissenschaftsverlag
• Bernhard Heinemann und Klaus Weihrauch: Logik für Informatiker, Teubner Stuttgart 1980
• M.Ruckert: Logik für Informatiker (Skriptum)