[AI-announce] Lehrveranstltungen der Gruppe "Logik und formale Verifikation"

[Thomas Zeume]

Liebe Studierende,

als Forschungsgruppe "Logik und Formale Verifikation" bieten wir in den 
kommenden Semestern die folgenden Lehrveranstaltungen an.  Wir freuen 
uns auf euren Besuch!

*Wintersemester 2022/2023*

(1) Informatik 3: Theoretische Informatik (Bachelor Pflicht-Modul)
Moodle-Kurs: https://moodle.ruhr-uni-bochum.de/course/view.php?id=47603

(2) Logik in der Informatik (Bachelor Wahlpflicht-Modul)
Moodle-Kurs: https://moodle.ruhr-uni-bochum.de/course/view.php?id=47604


*Sommersemester 2023 (geplant)*

(1) Model Checking (Bachelor Wahlpflicht-Modul)
Hilfreiches Vorwissen: Logik in der Informatik

(2) (Pro-)Seminar: Satisfiability
Hilfreiches Vorwissen: Logik in der Informatik


Viele Grüße
Thomas Zeume


*Informationen zur Veranstaltung "Logik in der Informatik"*

Logische Methoden spielen in vielen modernen Anwendungen der Informatik 
eine wichtige Rolle. Aus Datenbanken werden relevante Informationen  mit 
Hilfe auf Logik basierender Anfragesprachen extrahiert; die formale 
Verifikation von Software und Hardware basiert auf logischen 
Spezifikationssprachen und Algorithmen für diese; und Methoden für das 
automatisierte Schlussfolgern in der künstlichen Intelligenz haben ihre 
Grundlage in der formalen Logik.

In dieser Veranstaltung werden die formalen Grundlagen von modernen 
Logiken behandelt, mit einem Fokus auf ihrer Anwendung in der 
Informatik. Neben der klassischen Aussagenlogik und Prädikatenlogik 
betrachten wir auch Modallogik.  Für jede dieser Logiken formalisieren 
wir Syntax und Semantik, lernen wie sich informatische Szenarien in 
ihnen modellieren lassen, und betrachten Algorithmen und Kalküle für 
Unerfüllbarkeit und Folgerungsbeziehung.


*Informationen zur Veranstaltung "Model Checking"*

Wie kann die Korrektheit von Software und Hardware formal  überprüft 
werden? Im Model Checking werden Software- und Hardware-Module  durch 
Transitionssysteme formalisiert; gewünschte Eigenschaften mit Hilfe 
logischer Formalismen formal beschrieben; und mit Hilfe von Algorithmen 
automatisiert überprüft, ob ein Transitionssystem eine formal 
spezifizierte Eigenschaft besitzt.

In dieser Veranstaltung werden die theoretischen Grundlagen des Model 
Checkings vermittelt, mit einem Fokus auf logik-basierten 
Spezifikationssprachen. Die Spezifikationssprachen LTL und CTL werden 
eingeführt, ihre Ausdrucksstärke untersucht, und die wichtigsten 
algorithmischen Ansätze für das Model Checking vorgestellt.


*Informationen zum Seminar "Satisfiability"*

Das Erfüllbarkeitsproblem für logische Formeln — lässt sich eine 
gegebene logische Formel erfüllen? — ist eines der fundamentalen 
algorithmischen Probleme. Grund hierfür ist, dass sich viele andere 
wichtige algorithmische Probleme auf verschiedene Varianten des 
Erfüllbarkeitsproblems reduzieren lassen.

In diesem Seminar im Theoriebereich der Informatik wollen wir uns mit 
dem Erfüllbarkeitsproblem aus verschiedenen Perspektiven und für 
verschiedene Logiken beschäftigen.

Der Schwerpunkt wird auf dem Erfüllbarkeitsproblem für aussagenlogische 
Formeln und dem Erfüllbarkeitsproblem für (eingeschränkte) 
prädikatenlogische Formeln liegen:
* Das Erfüllbarkeitsproblem für aussagenlogische Formeln (SAT) ist die 
Grundlage der Theorie der NP-schwierigen Probleme: Jedes Problem aus NP 
lässt sich auf SAT zurückführen, ist also höchstens so schwierig wie 
SAT. Fortschritte beim Lösen von SAT übertragen sich deshalb auch in der 
Praxis oft auf andere Probleme aus NP.
* Das Erfüllbarkeitsproblem für (eingeschränkte) prädikatenlogische 
Formeln ist unter anderem die Grundlage für das Schlussfolgern in 
wissensbasierten Systemen und für die formale Verifikation von Hardware 
und Software. Für allgemeine prädikatenlogische Formeln ist das 
Erfüllbarkeitsproblem nicht algorithmisch lösbar (formal: 
unentscheidbar). In der Praxis werden daher oft eingeschränkte Klassen 
prädikatenlogischer Formeln benutzt, für die sich das Problem noch 
algorithmisch lösen lässt.