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)