Harald Ganzinger, Member Emeritus of WG1.3, died on June 3, 2004.

At the time of his death, Harald was scientific director at the Max-Planck-Institut für Informatik in Saarbrücken where he had been leader of the Programming Logics Group and honorary professor at the University of the Saarland since 1991. He had previously held a chair in Computer Science at the University of Dortmund.

His main field of research was automated deduction. His most recent work was on automatic tools for the verification of large hardware and software systems, namely the development of push-button methods for proving and disproving logical statements. He is also well known for the superposition calculus, a method that he developed in collaboration with Leo Bachmair for the efficient treatment of equational problems in automatic provers.

We all recall Harald as a very dynamic and active researcher, yet always so cheerful and ready to engage in discussions with colleagues and younger people! His profound contributions to Computer Science were just about to be celebrated, on July 7th, at IJCAR in Cork, where he was due to receive the Herbrand Award for his "seminal work on the theory underlying modern theorem proving systems; the breadth of his research covering nearly all major areas of deduction, and the depth of his results in each one of them; and his effective contributions to the development of systems and implementation techniques."

We shall all miss him very much.