Harald Ganzinger (31 October 1950, Werneck – 3 June 2004, Saarbrücken) was a German computer scientist who together with 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 the Herbrand Award in 2004 (posthumous) for his important contributions to automated theorem proving.