Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday

Jörg has had a major impact on our lives. I, Dieter, first met him in 1979 when I was an undergraduate student at the University of Karlsruhe, obliged to give a proseminar on Lenat's AM system. His inspiring enthusiasm and energy for this kind of AI system stirred my growing interest in automated theorem proving in general and guiding such provers in particular. Not surprisingly, after finishing my MSc thesis I registered as a PhD student of Christoph Walther and Peter Deussen, joining the development of the inductive theorem prover INKA. Years later, Jörg offered me a research position in Saarbrücken to incorporate proof guiding techniques into VSE; I accepted willingly.

At the time when Jörg moved to Karlsruhe I, Werner, was working in Wolfgang Menzel's group, which together with Deussen's group formed the institute of theoretical computer science. Despite countless controversial discussions on AI-related topics and developments in the common academic context, as well as ongoing changes in the German society of the early 1980s, we shared many basic views and soon became friends. But also, in a more restricted sense, my academic work was influenced by Jörg's often more than enthusiastic way of standing up for AI and, in particular, automated deduction. Being interested at that time in the semantics of programming languages and logics, the discussions with Jörg's group sharpened my view that computer-assisted deductive systems (together with "model based" analysis techniques) "animate" formal development techniques thereby enabling their application in software engineering.

Since then, our work at Jörg's research department at the DFKI has been guided by the search for a close integration of formal methodology and deductive support, bringing together two communities that, still today, are often far from working hand in hand. Throughout all the years, Jörg has been a constant source of inspiration, friendship and humor. In presenting Jörg with this book we hope that he will enjoy reading it, and since his work is by no means finished, we hope to return the favor by reading more of the essays he has promised to write in the coming years.