Maschinengestütztes Beweisen von Theoremen
Internationale Konferenz am Fachbereich für Mathematik und Informatik der Freien Universität Berlin vom 1. bis 7. August 2015
Nr. 141/2015 vom 27.05.2015
Die computergestützte Mechanisierung unterschiedlicher Logikformalismen ist Gegenstand einer Konferenz vom 1. bis 7. August 2015 am Fachbereich Mathematik und Informatik der Freien Universität Berlin. Unter dem Titel „Conference on Automated Deduction“ (CADE) befassen sich die Teilnehmer aus dem In- und Ausland vornehmlich mit der Methode des Automatischen Theorembeweisens. Dabei werden mathematische bzw. logische Beweise vollautomatisch durch den Computer gefunden. Unter Beweis wird hier eine präzise Argumentationskette verstanden, die ein Beweisziel (das Theorem) aus Grundannahmen (den Axiomen) ableitet. Erörtert wird auch, wie die automatische Deduktion beispielsweise in der Informatik und Mathematik angewendet werden kann. Teilnehmer sind renommierte Wissenschaftler führender Universitäten wie Oxford, Stanford und Carnegie Mellon. Die Special Session am 3. August ist öffentlich, die Veranstaltung wird sich mit der Vergangenheit, Gegenwart und Zukunft der Automatischen Deduktion befassen. Die ganze Konferenz ist medienöffentlich. Um Anmeldung unter info@cade-25.info wird gebeten.
Die CADE-Konferenz gilt als das weltweit führende Forum auf dem Gebiet der Automatischen Deduktion; sie feiert in diesem Jahr ihre 25. Auflage. Zu diesem Jubiläum integriert die CADE-Konferenz ein durch die Deutsche Forschungsgemeinschaft gefördertes Festkolloquium zum Thema „Past, Present and Future of Automated Deduktion“ (Vergangenheit, Gegenwart und Zukunft der Automatischen Deduktion). Im Rahmen der Konferenz werden weitere Veranstaltungen ausgerichtet: Es finden zehn internationale Workshops und sieben Fachtutorien, sowie drei Wettbewerbe statt, darunter die alljährlich organisierte Weltmeisterschaft im automatischen Beweisen von Theoremen. Zu den Höhepunkten der CADE-25-Konferenz gehört zudem die Verleihung eines internationalen Wissenschaftspreises, dem nach dem Logiker Jacques Herbrand (1908–1931) benannte Herbrand-Award.
Zeit und Ort
- Special Session: Montag, 3. August 2015, um 14.00 Uhr
- CADE: Samstag, 1. August 2015 bis Freitag, 7. August 2015
- Freie Universität Berlin, Fachbereich Mathematik und Informatik, Großer Hörsaal der Informatik, Takustr. 9, 14195 Berlin. U-Bahnhof Dahlem Dorf (U3)
Weitere Informationen
PD Dr. Christoph Benzmüller, Fachbereich Mathematik und Informatik der Freien Universität Berlin, E-Mail: info@cade-25.info