Harald Ganzinger (31 de octubre de 1950, Werneck - 3 de junio de 2004, Saarbrücken ) fue un científico informático alemán que junto con Leo Bachmair desarrolló el cálculo de superposición , que se utiliza (a partir de 2007) en la mayoría de los demostradores de teoremas automatizados de última generación para la lógica de primer orden .
En 1978 se doctoró en la Universidad Técnica de Múnich . Antes de 1991 fue profesor de informática en la Universidad de Dortmund . Poco después de su fundación en 1991 se incorporó al Instituto Max Planck de Informática de Saarbrücken . Hasta 2004 fue director del departamento de lógica de programación del Instituto Max Planck de Informática y profesor honorario de la Universidad del Sarre . Su grupo de investigación creó el demostrador automático de teoremas SPASS .
Recibió el Premio Herbrand en 2004 ( póstumo ) por sus importantes contribuciones a la demostración automatizada de teoremas .