Einführung in die Aussagenlogik, Prädikatenlogik, Logik-Programmierung und Temporale Logik

Fachkompetenzen
Die Studierenden:

• haben Kenntnisse über Syntax, Semantik und Anwendung von Aussagenlogik, Prädikatenlogik, Logik-Programmierung und Temporale Logik
• spezifizieren Probleme mit Hilfe von logischen Formeln
• lösen Fragen über aussagelogische Formeln mit Hilfe von Wahrheitstafeln
• ziehen logische Schlüsse der Aussagen- und Prädikatenlogik mit dem Kalkül des natürlichen Schließens
• beantworten Anfragen an Logik-Programme mit Hilfe der SLD-Resolution
• können Model-Checking von Kripke-Strukturen bezüglich CTL-Formeln algorithmisch durchführen

Methodenkompetenzen
Die Studierenden:

• erkennen Logik als ein vielseitiges Hilfsmittel in der Informatik

Sozialkompetenzen
Die Studierenden:

• arbeiten in kleinen Gruppen an Lösungen von Aufgaben
• präsentieren Lösungen von Aufgaben vor Gruppen

Selbstkompetenzen
Die Studierenden:

• erlernen Ausdauer bei der Bearbeitung schwieriger Aufgaben
• erlernen Präzision beim Aufschreiben von Lösungen

Die Vorlesung führt in die Aussagenlogik, Prädikatenlogik, Logik-Programmierung und Temporale Logik ein.
Ein gutes Verständnis von Logik ist für die Informatik von zentraler Bedeutung. Dieses wird bereits durch die weite Verbreitung der logischen Formelsprache in der Informatik belegt.

Zum Beispiel kommen einfache Boolesche Ausdrücke in jeder Programmiersprache und beim Schaltkreisentwurf vor; Horn-Klauseln werden zur Wissensrepräsentation eingesetzt; Formeln der Prädikatenlogik und Temporalen Logik werden zum Spezifizieren von Eigenschaften von Soft- und Hardware benutzt. Neuere Anwendungen wie interaktives und automatisches Beweisen sowie Logik-Programmierung und die damit verwandte Programmiersprache PROLOG unterstreichen den Werkzeugcharakter der Logik in der Informatik.

In der Vorlesung werden Syntax, Semantik, Verfahren und Kalküle zur Überprüfung der Gültigkeit von Formeln der Aussagenlogik, Prädikatenlogik und Temporalen Logik eingeführt und an Beispielen illustriert. Zentral ist der Begriff der logischen Folgerung.
Themen:

• Aussagenlogik: Syntax und Semantik, Wahrheitstafeln, natürliches Schließen
• Prädikatenlogik: Syntax und Semantik, natürliches Schließen
• Logik-Programmierung: deklarative und prozedurale Semantik, Unifikationsalgorithmus von Robinson, SLD-Resolution, PROLOG
• Temporale Logik CTL: Syntax und Semantik mittels Kripke-Strukturen, Algorithmus zum Model-Checking von CTL

Essentiell:
Skript "Logik"

Empfohlen:
D. van Dalen: Logic and Structure, Fourth Edition. Springer-Verlag, 2004.

Gute Sekundärliteratur:
U. Schöning. Logik für Informatiker, Spektrum Verlag, 2000.

Am Ende der Vorlesungszeit

Klausur oder mündliche Prüfung