Pflichtveranstaltungen

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

Grundlagenkurs zu formalen Methoden im Softwareentwurf: Modellierung, Spezifikation und Verifikation von Software