Harald Ganzinger - Harald Ganzinger
| Harald Ganzinger | |
|---|---|
| Née | 31 octobre 1950 
|
| Décédés | 3 juin 2004 (53 ans) |
Harald Ganzinger (31 Octobre 1950, Werneck - 3 Juin 2004, Sarrebruck ) était un Allemand informaticien qui, avec Leo Bachmair a développé le calcul de superposition , qui est (en 2007) utilisé dans la plupart de l'état de l'art automatisé prouveurs de théorèmes pour la logique du premier ordre .
Il a obtenu son doctorat. de l' Université technique de Munich en 1978. Avant 1991, il était professeur d'informatique à l' Université de Dortmund . Puis il a rejoint l' Institut Max Planck d'Informatique à Sarrebruck peu de temps après sa création en 1991. Jusqu'en 2004, il a été directeur du département Logique de programmation de l' Institut Max Planck d'Informatique et professeur honoraire à l'Université de la Sarre . Son groupe de recherche a créé le prouveur de théorème automatisé SPASS .
Il a reçu le prix Herbrand en 2004 (à titre posthume ) pour ses importantes contributions à la démonstration automatisée de théorèmes .
Les références
- Théorème équationnel basé sur la réécriture prouvant avec sélection et simplification , Leo Bachmair et Harald Ganzinger, Journal of Logic and Computation 3 (4), 1994.
Liens externes
- Page d'accueil personnelle de Harald Ganzinger - Version du 7 décembre 2013 enregistrée sur archive.org
 |
Cet article sur un informaticien allemand est un bout . Vous pouvez aider Wikipedia en le développant . |