Harald Ganzinger

from Wikipedia, the free encyclopedia

Harald Ganzinger (born October 31, 1950 in Werneck ( Bavaria ); † June 3, 2004 in Saarbrücken ) was a German computer scientist.

Harald Ganzinger studied mathematics with a minor in computer science at the University of Würzburg and the Technical University of Munich . When Jürgen Eickel he received his doctorate 1978th He completed his habilitation in 1983. A year later, he became a professor at the chair for translators and programming systems at the University of Dortmund . From 1991 until his death in 2004 he was director of the “Logic of Programming” working group at the Max Planck Institute for Computer Science in Saarbrücken . He is one of the most cited German authors in computer science and is on position 1727 on the CiteSeer list (as of August 2006). Ganzinger received the renowned Herbrand Award in 2004 . The award was given to him shortly before his death.


  • Rewrite-based equational theorem proving with selection and simplification
  • Resolution theorem proving
  • Basic paramodulation
  • Complexity analysis based on ordered resolution
  • Set constraints are the monadic class
  • DPLL (T): Fast decision procedures
  • Attributes coupled grammars


  • Kurt Mehlhorn, Uwe Waldmann, Reinhard Wilhelm: Harald Ganzinger October 31, 1950 - June 3, 2004. In: Max Planck Society, Yearbook 2005, pp. 107–108.

Web links

Individual evidence

  1. http://citeseer.ist.psu.edu/allcited.html