Harald Ganzinger (31 de octubre de 1950, Werneck - 3 junio de 2004, Saarbrücken ) era un alemán experto en informática que, junto con Leo Bachmair desarrolló el cálculo de superposición , que es (a partir de 2007) se utiliza en la mayor parte del estado de la técnica automatizada probadores de teoremas para la lógica de primer orden .
Harald Ganzinger | |
---|---|
Nació | 31 de octubre de 1950 |
Fallecido | 3 de junio de 2004 (53 años) |
Recibió su Ph.D. de la Universidad Técnica de Munich en 1978. Antes de 1991 fue profesor de Ciencias de la Computación en la Universidad de Dortmund . Luego se unió al Instituto Max Planck de Ciencias de la Computación en Saarbrücken poco después de su fundación en 1991. Hasta 2004 fue Director del departamento de Lógica de Programación del Instituto Max Planck de Ciencias de la Computación y profesor honorario en la Universidad de Saarland . Su grupo de investigación creó el demostrador automático de teoremas SPASS .
Recibió el premio Herbrand en 2004 ( póstumo ) por sus importantes contribuciones a la demostración automatizada de teoremas .
Referencias
- Demostración del teorema de la ecuación basada en la reescritura con selección y simplificación , Leo Bachmair y Harald Ganzinger, Journal of Logic and Computation 3 (4), 1994.