Vorlesung über "Erfüllbarkeitstester"

Ewald Speckenmeyer

Die Vorlesung findet donnerstags 11.00-12.30 Uhr in Seminarraum 616, Pohligstr. 1 statt.

Das Erfüllbarkeitsproblem der Aussagenlogik bildet das algorithmische Kernproblem verschiedener Anwendungen. Erwähnt seien die als Bounded Model Checking bekannte Verifikationstechnik für Schaltkreise, Konfigurationsprobleme oder Planungsprobleme.

In der Vorlesung werden die Grundlagen von Erfüllbarkeitstestern vorgestellt, sowie verschiedene leistungsfähige Tester behandelt. Darüberhinaus wird die Einbeziehung domänenspezifischen Wissens in solche Tester besprochen.

Evtl. Fragen können Sie per E-Mail an Prof. E. Speckenmeyer richten.

Das Thema behandelt ein aktuelles Forschungsgebiet der Arbeitsgruppe. Die behandelten Themen sollen dazu beitragen, leistungsfähige Tester für ausgesuchte Anwendungen zu entwickeln. Nützlich für den Einstieg in das Thema ist das Buch:

• Kleine Büning/Lettmann: Aussagenlogik: Deduktion und Algorithmen. Teubner 1994

Obiges Buch ist z.Zt. nicht mehr im Handel verfügbar; die englische Übersetzung ist direkt von Cambridge University Press beziehbar:

• Kleine Büning/Lettmann: Propositional Logic: Deduction and Algorithms. Cambridge University Press 1999