Seite - 322 - in Reflexionen vor Reflexen - Memoiren eines Forschers

322 KAPITEL4. FORSCHERLEBEN genannteConstablewar einer unter ihnen. Sein damals inLaibach vonmir gehörterVor- tragkann inmeinemLebenalsder auslösendeFunke zumeiner endgültigen Identifikation mit dem sich daraus ergebenden langfristigenForschungsprogrammangesehenwerden. KonkretbestanddasForschungsprogrammfürmich inderWeiterentwicklungundVer- besserungmeines 1970 inDetroit selbst entwickeltenBeweiserprogrammsunddessenAn- wendung auf die Programmierung.Weitmehr als einDutzend von Studenten haben da- mals in diesem Forschungsprogramm vor allem beim Beweiserbaumitgewirkt. Dies hat uns innerhalb des InstitutsHerr Samelsonmit seinerProtektion undwohlwollendenFör- derungermöglicht.Formalwarenwir imÜberregionalenForschungsprogrammInformatik (ÜRF)desBundesministers fürForschungundTechnologie (BMFT)weiterhinunterdem Thema Mechanisierung inderMathematik angesiedelt.ProgrammierthabendieStuden- tenmeist inALGOL60, einerProgrammiersprache, die imGegensatz zudem inMünchen leider nicht verfügbarenSNOBOL4 für solchenicht-numerischeAufgabenstellungen recht sperrig und daher nicht allzu geeignet war. Die Brücke hin zur Programmierungwar zu jener Zeit erst einmal noch ganzmeine eigene Forschungsangelegenheit. 1974machte ich michandieErarbeitung einerHabilschrift zugenaudieser kombiniertenThematik, deren inhaltlicheGrobstruktur etwaMitte 1974 erarbeitet war.64EndeDezember 1974war die Arbeit fertiggestellt. Bevor ich auf den Inhalt undBeitrag dieser Schrift eingehe, seien noch besondereVor- kommnisse auf zwei der bereits genanntenKonferenzen erläutert, die ich imLaufe dieses Jahres 1974besuchte.Wie bereits erwähnt präsentierte ich dieErgebnisse zuunseren au- tomatischenBeweisernaufderACMKonferenz,die imFebruar1974 inDetroit stattfand. AmEndemeinesVortrags stellte von ganz hinten imSaal einDiskutant eine eingehende Frage, die ich trotzRückfrageundAntwort darauf akustischnicht genaugenugverstehen konnte,wasaberauchandernicht seltenunmöglichenundunüberlegtarrogantenArtder Amerikaner gelegenhabendürfte von jedermann zu erwarten, daß er auch ohnebesonde- reAnstrengungdes Sprechendendessen amerikanischenSlang einfach zu verstehenhabe. Der Sitzungsleiter empfahl uns beiden eine persönlicheAussprache darüber imAnschluß an die Sitzung. So kam der Diskutant danach zumir, stellte sich als Don Loveland vor und verabredete sich mit mir in seinem Hotelzimmer zu einem intensiveren fachlichen Austausch. 64ImBericht des SenatsbeauftragtenF.L.Bauer vom1.7.1974 zumStanddesForschungsvorhabens im ÜberregionalenForschungsprogrammInformatik (ÜRF)desBundesministers fürForschungundTechno- logie (BMFT) findet sich auf S.10 unter der Überschrift Programmsynthese bereits die Thematik der Anwendbarkeit desKleene-Nelson-Theorems aufgeführt, das in derAnwendung vonBeweisverfahren für die Programmierung eine zentraleRolle spielt.