German computer scientist

Harald Ganzinger (31 October 1950, Werneck – 3 June 2004, Saarbrücken) was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is (as of 2007) used in most of the state-of-the-art automated theorem provers for first-order logic.

He received his Ph.D. from the Technical University of Munich in 1978. Before 1991 he was a Professor of Computer Science at University of Dortmund. Then he joined the Max Planck Ins*ute for Computer Science in Saarbrücken shortly after it was founded in 1991. Until 2004 he was the Director of the Programming Logics department of the Max Planck Ins*ute for Computer Science and honorary professor at Saarland University. His research group created the SP* automated theorem prover.

He received the Herbrand Award in 2004 (posthumous) for his important contributions to automated theorem proving.

References

• Rewrite-Based Equational Theorem Proving with Selection and Simplification, Leo Bachmair and Harald Ganzinger, Journal of Logic and Computation 3(4), 1994.

External links

• Personal Homepage of Harald Ganzinger — Version of Dec.7th, 2013 saved at archive.org