Logik-Kalküle
Fakultät für Informatik und Mathematik ©
Name Logik-Kalküle
Verantwortlich Prof. Dr. Martin Ruckert
SWS 4
ECTS 5
Sprache(n) Deutsch
Englisch
Lehrform SU mit Übung
Angebot im Wechsel mit anderen Fächern der gleichen Fachgruppe
Aufwand

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

Voraussetzungen

Keine

Ziele

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.

Inhalt

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.

Medien und Methoden

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

Literatur
  • 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)
Zuordnungen Curricula
SPO Fachgruppe Code ab Semester Prüfungsleistungen
IG Version 2010 CGBV: Theoretische Grundlagen IG-TTI-0050 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2010 EC: Theoretische Grundlagen IG-TTI-0050 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2010 SWE: Theoretische Grundlagen IG-TTI-0050 1 benotete schriftliche Prüfung 90 Minuten
IS Version 2009 WPF Informatik und Wirtschaft IF-S-M-I09 1 benotete schriftliche Prüfung 90 Minuten
IS Version 2017 WPF Informatik und Wirtschaft IF-S-M-I09 1 benotete schriftliche Prüfung 90 Minuten