Chair of Programming Languages and AI
print
Breadcrumb Navigation
Content

Logik für Informatiker

Dozent: François Bry
Sprache: Deutsch
Zeitraum: Vom 31.03.2025 bis zum 11.04.2025 jeden Werktag von 09:00 Uhr bis 13 Uhr

Inhalt

Methoden und Ansätze, die auf der Logik beruhen, sind nicht nur in der theoretischen Informatik, sondern auch in der praktischen Informatik allgegenwärtig, wie die Verbreitung von Begriffen wie etwa „Programmverifikation", „Wissensrepräsentation", „Model Checking", „Field Programmable Logic" bezeugt.

Das Masterseminar bietet eine Einführung in die Logik für Masterstudent:innen der Informatik. Um ein möglichst breites Publikum – und nicht nur die Aficionados von Mathematik und Theorie – zu erreichen, soll neben einem „Leitfaden", der in die Syntax, Semantik
und Beweistheorie der Aussagen- und Prädikatenlogik erster Stufe einführt, „Exkurse", Anwendungen der Logik in der Informatik – z.B. in relationalen Datenbanken – oder Vertiefungen – z.B. Prädikatenlogik höherer Stufe – gewidmet sein.

Ein Skriptum des Dozenten soll als Grundlage der Seminarvorträge dienen.

Themen:

 

1 Syntax

  • Aussagenlogik
  • Exkurs: Präfix- und Postfixnotation und Präzedenzen
  • Prädikatenlogik erster Stufe
  • Exkurs: Termdarstellungen in Programmier- und Modellierungssprachen
  • Exkurs: Das Entitäts-Relations-Modell und der Tupel-Kalkül
  • Exkurs: UML und OCL
  • Beschränkte Quantifikation
  • Exkurs: Regelbasierte Formalismen
  • Exkurs: Mehrsortige Prädikatenlogik erster Stufe
  • Exkurs: Prädikatenlogik zweiter Stufe und höherer Stufen
  • Exkurs: Syntax von Modal- und Temporallogiken

2 Semantik

  • Boole'sche Funktionen
  • Exkurs: Schaltkreise und Boole'sche Algebren
  • Interpretationen und Modelle aussagenlogischer Formeln
  • Exkurs: Natürlichsprachliche Interpretationen der Junktoren
  • Interpretationen und Modelle von Formeln der PL1S
  • Gleichheit
  • Exkurs: Natürlichsprachliche Interpretationen der Quantoren
  • Herbrand-Interpretationen und Skolemisierung
  • Exkurs: Relationale Datenbanken
  • Die natürlichen Zahlen und das Induktionsaxiom
  • Exkurs: Semantik von Modal- und Temporallogiken

3 Beweistheorie

  • Entscheidbarkeitsergebnisse für die Aussagenlogik
  • Exkurs: Logikkalküle
  • Normalformen
  • Exkurs: Die Davis-Putnam-Beweismethode
  • Entscheidbarkeitsergebnisse für die PL1S
  • Exkurs: Die PUHR-Tableau-Beweismethode
  • Exkurs: Deklarative Semantik von definiten Logikprogrammen
  • Der Endlichkeitssatz
  • Exkurs: Folgerung im Endlichen- Nichtausdrückbarkeit des Induktionsaxioms in der PL1S