Harald Ganzinger - Harald Ganzinger

Harald Ganzinger (31. října 1950, Werneck - 3. června 2004, Saarbrücken ) byl Němec počítačový vědec kdo spolu s Leo Bachmair vyvinul superpoziční počet, který se (od roku 2007) používá ve většině nejmodernějších technologií automatizované věty provers pro logika prvního řádu.

Dostal svůj Ph.D. z Technická univerzita v Mnichově v roce 1978. Před rokem 1991 působil jako profesor informatiky na University of Dortmund. Pak se připojil k Max Planck Institute for Computer Science v Saarbrücken krátce poté, co byla založena v roce 1991. Do roku 2004 působil jako ředitel odboru programovací logiky VŠE Max Planck Institute for Computer Science a čestný profesor na Sárská univerzita. Jeho výzkumná skupina vytvořila SPASS automatizovaný testovací teorém.

Obdržel Herbrand Award v roce 2004 (posmrtný ) za jeho důležité příspěvky pro automatizované dokazování věty.

Reference

externí odkazy