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

302 KAPITEL4. FORSCHERLEBEN zudenRechnernderUniversity ofMichigan inAnnArbor.Diesewar eineder drei ersten Universitäten, die an das 1969 gestartete ARPANetz angeschlossen wurden und damit das email-ZeitalterAnfang 1971 inGang setzten. So lernte ich schonbald dieBenutzung meinerWorkstation zumVersendenvon emails kennenundgehöre damit zudenweltweit allererstenNutzern dieses heute jedermann geläufigenKommunikationsmediums. AuchwennangesichtsdesbeschriebenenAufgabenpensumsfastkeineZeit fürdieeigene Forschung übrig blieb, konnte ich doch zwei sehr unterschiedliche Ergebnisse erarbeiten. Daserstebesteht ineinerErweiterungeinervonScottundStracheyvorgeschlagenenSpra- che zurFormalisierungder Semantik vonProgrammiersprachen.DieErweiterungbetrifft die Hinzunahme von Sprüngen (Gotos), die von diesenAutoren nicht berücksichtigt wa- ren.36DasErgebnis habe ich sowohlDanaScott als auchManfredPaulmitgeteilt.Deren Reaktionen darauf habenmich aber nicht zurweiterenVerfolgung dieser Forschungsrich- tung ermutigt. Allerdings habe ich imGefolge und zumweiterenAustauschDana Scott zu einemKolloquiumsvortrag an unser Institut eingeladen. Dieser wurde mitten in sei- nemVortrag durch einen recht deplatziertenEinwand eines Zuhörers so verärgert, daß er erbost den Saal verließ und so auf den Rest seiner Rede zur Enttäuschung der Zuhörer einfach verzichtete. Scott war eine Primadonna, die als solche behandelt werden wollte, wasderZuhörer bei seinemEinwand leidermißachtete.EinderartigesVerhaltenhabe ich bei akademischenVorträgen nur dieses eineMal erlebt. Mein eigentliches wissenschaftliches Interesse galt aber, wie weiter oben schon kurz ausgeführt, dem Gebiet des Automatischen Beweisens. Schon im Laufe meiner Arbeit inMünchen hatte ichmir, ausgehend von demmir wohlvertrauten formalen System der Prädikatenlogik von Schütte, das Vorgehen eines solchen Beweisers zurechtgelegt. An- gesichts der hervorragenden Rechnerausstattung bot sich mir nun die Gelegenheit, auf dieserGrundlage ein Beweisersystem zu programmieren. SeymourWolfson empfahlmir, dazudie auf unseremSystemvorhandeneProgrammierspracheSNOBOL4zuverwenden. Ende1970 lief dannmein erstesBeweiserprogrammfürdiePrädikatenlogik.37DasErgeb- nis wollte ich zur zweiten IJCAI-1971 in London einreichen, wozu damals ebenfalls ein Abstrakt genügte.Aufgrund sehr unglücklicherUmstände, verursacht nicht zuletzt durch 36WolfgangBibel,Mathematical Semantics for a LanguagewithGOTOS,Okt. 1970, unveröffentlicht. Die Arbeit wurde am 17.12.1970 als Abstrakt bei einer Konferenz in Hawai eingereicht, dort aber von dessenProgramChairM.A.Harrison nicht angenommen. 37Das Programmmit dem Namen PRV ist geschrieben in der Programmiersprache SNOBOL4 und umfaßt 219 Programmzeilen. Es befindet sich heute im elektronischen Museum für Theorembeweiser (http://theoremprover-museum.github.io/).