Harald Ganzinger was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is used in most of the state-of-the-art automated theorem provers for first-order logic.