Modul

Siehe Teilleistung.

Nach Abschluss des Moduls verfügen Studierende über folgende Kompetenzen. Sie …

• kennen und verstehen die vorgestellten logischen Grundkonzepte und Begriffe, insbesondere den Modellbegriff und die Unterscheidung von Syntax und Semantik,
• können natürlichsprachlich gegebene Sachverhalte in verschiedenen Logiken formalisieren sowie logische Formeln verstehen und ihre Bedeutung in natürliche Sprache übersetzen,
• können die vorgestellten Kalküle und Analyseverfahren auf gegebene Fragestellungen bzw. Probleme sowohl manuell als auch mittels interaktiver und automatischer Werkzeugunterstützung anwenden,
• kennen die grundlegenden Konzepte und Methoden der formalen Modellierung und Verifikation,
• können Programmeigenschaften in formalen Spezifikationssprachen formulieren, und kleine Beispiele mit Unterstützung von Softwarewerkzeugen verifizieren.
• können beurteilen, welcher logische Formalismus und welcher Kalkül sich zur Formalisierung und zum Beweis eines Sachverhalts eignet

Siehe Teilleistung.

Logikbasierte Methoden spielen in der Informatik in zwei Bereichen eine wesentliche Rolle: (1) zur Entwicklung, Beschreibung und Analyse von IT-Systemen und (2) als Komponente von IT-Systemen, die diesen die Fähigkeit verleiht, die umgebende Welt zu analysieren und Wissen darüber abzuleiten.

Dieses Modul

• führt in die Grundlagen formaler Logik ein und
• behandelt die Anwendung logikbasierter Methoden
  • zur Modellierung und Formalisierung
  • zur Ableitung (Deduktion),
  • zum Beweisen und Analysieren

von Systemen und Strukturen bzw. deren Eigenschaften.

Mehrere verschiedene Logiken werden vorgestellt, ihre Syntax und Semantik besprochen sowie dazugehörige Kalküle und andere Analyseverfahren eingeführt. Zu den behandelten Logiken zählen insbesondere die klassische Aussagen- und Prädikatenlogik sowie Temporallogiken wie LTL oder CTL.

Die Frage der praktischen Anwendbarkeit der vorgestellten Logiken und Kalküle auf Probleme der Informatik spielt in dieser Vorlesung eine wichtige Rolle. Der Praxisbezug wird insbesondere auch durch praktische Übungen (Praxisaufgaben) hergestellt, im Rahmen derer Studierende die Anwendung aktueller Werkzeuge (z.B. des interaktiven Beweisers KeY) auf praxisrelevante Problemstellungen (z.B. den Nachweis von Programmeigenschaften) erproben können.

Siehe Teilleistungen.

Der Gesamtarbeitsaufwand für dieses Modul beträgt 180h.

Der Aufwand setzt sich zusammen aus:

34,5h = 23 * 1,5hVorlesung (Präsenz)

10,5h = 7 * 1,5h Übungen (Präsenz)

60h Vor- und Nachbereitung, insbes. Bearbeitung der Übungsblätter

40h Bearbeitung der Praxisaufgaben

35h Klausurvorbereitung