Kenntnisse in den Grundlagen der mathematischen Logik, insbesondere hinsichtlich automatisierbaren Beweisverfahren und deren Anwendungen. Die Teilnehmer lernen exemplarisch die Grundlagen, Möglichkeiten und Grenzen von Logik-basierten Beweisverfahren in der Informatik kennen. Sie werden befähigt, moderne Verifikationsverfahren in der Industrie einzuführen und anzuwenden (z.B. Hardware- und Software-Verifikation, Konfiguration von Kraftfahrzeugen).
- Grundlagen: Terme und Induktion
- Aussagenlogik: Entscheidungsverfahren und Anwendungen (Resolution, SAT-Solving, BDD, Konfiguration von Kraftfahrzeugen)
- Prädikatenlogik: Beweisverfahren und Anwendungen (Resolution, Prolog)
- Spezielle Logiken: Beweisverfahren und Anwendungen (Hoare-Kalkül, Software-Verifikation)
