Harald Ganzinger

Harald Ganzinger (October 31 1950 - June 3 2004) was a German computer scientist that 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 Institute 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 Institute for Computer Science and honorary professor at Saarland University. His research group created the SPASS automated theorem prover.

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

References

*" [http://logcom.oxfordjournals.org/cgi/content/abstract/4/3/217 Rewrite-Based Equational Theorem Proving with Selection and Simplification] ", Leo Bachmair and Harald Ganzinger, Journal of Logic and Computation 3(4), 1994.

External links

* [http://www.mpi-inf.mpg.de/~hg Personal Homepage of Harald Ganzinger]
* [http://www.mpi-inf.mpg.de/departments/d2/ The Programming Logics Department of the Max Planck Institute for Computer Science]