Lernziele der Veranstaltung

siehe TUCAN

Lehrinhalte:
Syntax und Semantik der Aussagenlogik, funktionale Vollständigkeit und Normalformen, Kompaktheitssatz der Aussagenlogik, vollständige Beweiskalküle: Resolution und ein Sequenzenkalkül;

Syntax und Semantik der Logik erster Stufe, Strukturen und Belegungen, Normalformen und Skolemisierung, der Satz von Herbrand und der Kompaktheitssatz der Logik erster Stufe, vollständige Beweiskalküle: (Grundinstanzen-)Resolution und ein Sequenzenkalkül,
Gödelscher Vollständigkeitssatz, Unentscheidbarkeit der Logik erster Stufe;

optional: Exkurse zu Ausdrucksstärke und model checking

Modellierung nebenläufiger Software mit der Sprache ProMeLa, Formalisierung von Sicherheits- und Lebendigkeitseigenschaften mit temporaler Aussagenlogik, Theoretische Grundlagen von Modellprüfungsverfahren, Verifikation von ProMeLa Programmen mittels des Modellprüfers SPIN, Syntax, Semantik und Sequenzenkalkül für typisierte Logik erster Stufe, Grundlagen der kontraktbasierten Softwarespezifikationssprache JML, Dynamische Logik als eine Programmlogik erster Stufe, Formale Programmverifikation durch symbolische Ausführung und Invariantenschließen, Werkzeugunterstützte Verifikation von Java-Programen mit der KeY System

Moodlekurs zur Lehrveranstaltung Informationsmanagement, ehem. Einführung in Data and Knowledge Engineering (20-00-0015) sowie zu Allgemeine Informatik III. Zum Einschreiben benötigen Sie ein Passwort, das in der ersten Vorlesung bekannt gegeben wird und über die Vorlesungszeit vor der Tür zu Raum S202/B113 aushängt.

Auf diesen Kurs können nur die Tutor_innen der Rechnerorganisation im Sommersemester 2017 zugreifen.