Die Vorlesung führt in die grundlegenden Begriffe der mathematischen Logik ein, die in der Informatik vielfältig Anwendung finden. Sie vermittelt Kenntnisse, die in vielen Informatik-Vorlesungen des Hauptstudiums vorausgesetzt werden  u.a. in den Vorlesungen über Automatentheorie, rechnergestütztes Beweisen, Logikprogrammierung, Wissensrepräsentation und Übersetzerbau.

Behandelt werden: Syntax der Aussagenlogik und Prädikatenlogik erster Stufe, Interpretationen und Modelle von Formeln, der Sequenzenkalkül, die Beweismethode der Resolution und ihre Anwendung. Der Vollständigkeitssatz und der Kompaktheitssatz. Die behandelten Konzepte werden anhand des Theorembeweisers PVS illustriert. Dieser bietet die Möglichkeit, mit formalen Beweisen praktisch umzugehen und das rigorose Beweisen handwerklich zu erlernen. Ausblicke auf den Gödelschen Unvollständigkeitssatz (vulgo: "es gibt wahre Aussagen, die sich nicht beweisen lassen") und Speziallogiken, die in der Wissensrepräsentation und der automatischen Verifikation eine Rolle spielen, runden die Veranstaltung ab.