CADE-25: Computer-Logiker treffen sich in Berlin
Heute startet in der Freien Universität Berlin die 25. Internationale "Conference on Automated Deduction", auf der die jüngsten Fortschritte bei computergestützten Beweisverfahren diskutiert werden.
(Bild: CADE)
- Ralf BĂĽlow
- Wolfgang Kreutz
Zu den Wurzeln der Künstlichen Intelligenz zählt die Mechanisierung der Logik. Schon das 19. Jahrhundert kannte "Denkmaschinen", die einfache Schlüsse zogen. Die Ära der Computer brachte zudem Programme, die korrekte Aussagen der Prädikatenlogik bewiesen. Ab 1974 fanden dann weltweit Konferenzen zur automatischen Deduktion statt, die mit dem Kürzel CADE zusammengefasst werden.
Die mittlerweile 25. Tagung der Reihe, CADE-25, beginnt am heutigen Samstag im Institut für Informatik der Freien Universität Berlin. Sie umfasst diverse Untertagungen und dauert bis Freitag, dem 7. August. Hauptorganisator ist der Logiker Christoph Benzmüller, dessen Bestätigung des Gödelschen Gottesbeweises vor zwei Jahren Aufsehen erregte.
Die ersten zweieinhalb Tage der Konferenz bringen Workshops und Tutorials; am Montag folgen ab 14 Uhr Vorträge zur Vergangenheit, Gegenwart und Zukunft des maschinellen Beweisens, die auch der Öffentlichkeit zugänglich sind. Anlass ist der fünfzigste Geburtstag der Resolution, der vom Engländer John Alan Robinson erfundenen Ableitungsmethode für die Aussagen- und die Prädikatenlogik, die die Computerdeduktion erst praktikabel machte.
Robinson stützte sich bei seinem Kalkül auf Ideen des französischen Mathematikers Jacques Herbrand, der 1931 mit 23 Jahren beim Bergsteigen den Tod fand. Nach ihm ist die wichtigste Auszeichnung für Computerlogiker benannt, der Herbrand-Preis, der auf der Berliner Tagung dem in Manchester lehrenden Andrei Voronkov verliehen wird. Voronkov entwickelte unter anderem das prädikatenlogische Beweisprogramm Vampire.
In Schwung kommt die Konferenz am Montagabend mit einem Empfang im Berliner Botanischen Garten; angesagt sind ein Grußwort der Bundestagsabgeordneten und Mathematikerin Ute Finckh-Krämer und ein Vortrag von KI-Veteran Wolfgang Bibel. Die restlichen CADE-25-Tage füllen insgesamt zehn Sitzungen, mehrere Exkursionen und eine zweite Abendveranstaltung, wo der Informatiker Jörg Siekmann referiert. Details zu allen Programmpunkten liefert eine 24seitige PDF-Broschüre. (wre)
