| Termine: | VL Mi 11 - 13 (Rud. 3.110) J. Köbler und O. Beyersdorff |
|---|
| Zuordnung: | Hauptstudium, Halbkurs (1. Teil) |
|---|
Die Vorstellung, Beweise für mathematische Sätze auf mechanischem
Wege finden zu können, hat schon seit langer Zeit faszinierende Wirkung
ausgeübt. Heute finden automatisierte Beweissysteme vielfach Anwendung
in der Informatik, vor allem der künstlichen Intelligenz.
In der Vorlesung, die sich auf die Aussagenlogik beschränkt, werden zunächst verschiedene Beweissysteme (wie z.B. Resolution, Frege- Systeme u.a.) zusammen mit Algorithmen zum effizienten Aufsuchen von Beweisen aussagenlogischer Tautologien vorgestellt. Daneben soll der Beweislänge als Parameter Beachtung geschenkt werden: gibt es für ein gegebenes Beweissystem wahre Aussagen, für die sich kein kurzer Beweis in diesem System finden läßt? Hierdurch werden Querbezüge zu Fragen der Komplexitätstheorie (z.B. dem P-NP Problem) hergestellt, auf die näher eingegangen wird.
Vorkenntnisse, wie sie im Grundstudium erworben werden, sind zum Besuch
der Vorlesung ausreichend. Die Vorlesung wird im Sommersemester durch einen
zweiten Teil zu einem Halbkurs ergänzt.
| [1] | S. R. Buss (ed.), Handbook of Proof Theory, North-Holland, 1999. |
| [2] | S.R. Buss, Propositional Proof Complexity, An Introduction. |
| [3] | P. Beame, T. Pitassi, Propositional Proof Complexity. Past, Present, and Future. |
| [4] | H. Kleine Büning, T. Lettmann, Aussagenlogik: Deduktion und Algorithmen, Teubner, 1994. |
| [5] | J. Krajicek, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, 1995. |