Das Seminar vertieft Themen aus den Vorlesungen "SAT-Solving und Anwendungen" und "Automatisches Beweisen". Mögliche Vortragsthemen gibt es u.a. auf den Gebieten Normalformen, Boolesche Quantoren-Elimination, SAT basierte Optimierung, Bounded Model Checking und Software Verifikation.