Харальд Ганцингер (31 октября 1950 г., Вернек - 3 июня 2004 г., Саарбрюккен ) был немецким компьютерным ученым, который вместе с Лео Бахмаром разработал исчисление суперпозиции , которое (по состоянию на 2007 год) используется в большинстве современных автоматизированных Средства доказательства теорем для логики первого порядка .
Харальд Ганзингер | |
---|---|
Родившийся | 31 октября 1950 г. |
Умер | 3 июня 2004 г. (53 года) |
Он получил докторскую степень. окончил Технический университет Мюнхена в 1978 году. До 1991 года он был профессором компьютерных наук в Дортмундском университете . Затем он присоединился к Институту компьютерных наук Макса Планка в Саарбрюккене вскоре после его основания в 1991 году. До 2004 года он был директором отдела логики программирования Института компьютерных наук Макса Планка и почетным профессором Саарландского университета . Его исследовательская группа создала автоматическое средство доказательства теорем SPASS .
Он получил премию Хербранда в 2004 году ( посмертно ) за свой важный вклад в автоматическое доказательство теорем .
Рекомендации
- Основанное на перезаписи доказательство теорем с отбором и упрощением , Лео Бахмар и Харальд Ганцингер, Журнал логики и вычислений 3 (4), 1994.