Page - 286 - in Reflexionen vor Reflexen - Memoiren eines Forschers

286 KAPITEL4. FORSCHERLEBEN allerdingsschoneinJahrspäternachSaarbrückenberufenwurde.Darüberhinausumfaßte sie noch Herrn JoachimCiesinger und FrauDorisMaison. Die letztere versuchte kateg- orientheoretischeBerechnungen zumechanisieren. IhreVorstellungendazuhatte auch im späterenVerlauf niemand von unswirklich verstanden.NachmeinerKenntnis ist daraus auch nie etwas Konkretes, nicht einmal ein interner Report entstanden. Herr Ciesinger hatte damals noch keine ausgeprägte Zielrichtung für seine angestrebte Promotion, die sich dann später mit der Thematik der Compiler Generierung befaßte, was ersichtlich mit der Mechanisierung in der Mathematik nichts zu tun hatte. Weder Samelson noch Langmaack konnten auf demGebiet der Arbeitsgruppe irgendeine fachliche Kompetenz vorweisen. Auch eine Projektbeschreibung dazu war als Vorlage nicht verfügbar. Kurz, inhaltlich schlingerte die Arbeitsgruppe zumZeitpunktmeines Eintritts recht ziellos vor sich hin. Fürmich ergab sich daraus ein einmaliger Freiraum für die Gestaltungmeiner eigenenForschungen. IcharbeitetemichvorallemindieLiteraturdesAutomatischenBeweisensein. Indiesem Fachgebiet versuchteman,mathematischeBeweise automatisch vonRechnern erarbeiten zu lassen.VonHerrnSamelson erhielt ichhierzu sehr guteLiteraturhinweise. So studierte ichRobinsonsResolutionebensowiedie einschlägigenArbeitenvonHaoWang,StigKan- gerundDagPrawitz. ImSommer1969organisierteunser InstitutamChiemseeeinTreffen von deutschen Informatikern, deren Forschungsarbeit von der Deutschen Forschungsge- meinschaft (DFG)unddemerstendeutschenDV-Programmfinanziell unterstütztwurde. Bei dieser Gelegenheit lernte ich Gerd Veenker von der Universität Tübingen kennen, der bereits seit einemknappen Jahrzehnt auf diesemGebiet gearbeitet undmit entspre- chendenArbeiten diplomiert undpromoviert hatte.16 Infolgemeiner fundierten logischen Vorkenntnisse sowie all dieser Anregungen stabilisierte sich die Zielrichtungmeiner For- schungsarbeit sehr raschvor allemaufdiesemaussichtsreichenGebiet, auchwenn oder geradeweil sich inmeinemUmfeld so gutwie niemand dafür interessierte. UmdieKontaktemitdenLogikernnichtganzabreißenzu lassen, trug icham11.7.1969 auf Einladung von HerrnWalther Oberschelp imMathematischen Kolloquium der TH HannoverüberdieErgebnissemeinerDissertationvor.Wie schon indenVorjahrennahm ich bereits in den allerersten Monaten meiner Tätigkeit an der TUM am Bayerischen Mathematiker Kolloquium inMemmingen teil, das ich schon im vorangegangenen Jahr 1968 zusammenmit denKollegen bei Schütte, damals in Eichstätt, besucht hatte. Auch 16Eine ausführliche Darstellung der Leistungen von Herrn Veenker findet sich im Abschnitt 4 der Arbeit: Wolfgang Bibel, Early History and Perspectives of Automated Deduction. Proceedings of the 30thAnnualGermanConference onArtificial Intelligence (KI-2007), J.Hertzberg,M.Beetz,R.Englert Hrsg., September 10 13,Osnabrück, LNAI,Vol. 4667, Springer, Berlin, 2 18 (2007).