Harald Ganzinger

D2: Programming Logics Group

Harald Ganzinger (1950 - 2004)

Max-Planck-Institut für Informatik
Scientific Director

Prof. Dr. Harald Ganzinger died on June 3, 2004 after a long and serious illness.

If you are interested in Harald Ganzingers work, please contact:

Prof. Dr. Christoph Weidenbach
Campus E1 4, Room 612 (Building E1 5)
66123 Saarbrücken

Email:  weidenbach@mpi-inf.mpg.de
Phone: +49 681 9325 900
Fax: +49 681 9325 999

Research Topics

  • Term Rewriting
  • Saturation-based Theorem Proving
    • Transitivity, Equality, first-order Theorem Proving, Redundancy and Simplification, algebraic Refinements
  • Decidable Fragments of first-order Logic
    • Constraint Logics, Word Problems, Decision Procedures, Complexity
  • Automated Complexity Analysis
    • Meta-comlexity Theorems, logic Programming with guaranteed Complexity, Complexity Analysis through Saturation



  • The Saturate System: an experimental prover for first-order logic over transitive relations
  • SPASS: a high-performance prover for first-order logic with equality
    Try WebSPASS!


  • Harald Ganzinger has been member of the Program Committees of the following recent Conferences:

Former Students