Харальд Ганзингер

Харальд Ганзингер
Рожденный	31 октября 1950 г.
Умер	3 июня 2004 г. (53 года)
Альма-матер	Технический университет Мюнхена

Харальд Ганцингер (31 октября 1950, Вернек — 3 июня 2004, Саарбрюккен ) — немецкий учёный-компьютерщик , который вместе с Лео Бахмайром разработал исчисление суперпозиции , которое (по состоянию на 2007 год) используется в большинстве современных автоматизированных систем. средства доказательства теорем для логики первого порядка .

Он получил докторскую степень. окончил Технический университет Мюнхена в 1978 году. До 1991 года он был профессором компьютерных наук в Дортмундском университете . Затем он присоединился к Институту компьютерных наук Макса Планка в Саарбрюккене вскоре после его основания в 1991 году. До 2004 года он был директором отдела логики программирования Института компьютерных наук Макса Планка и почетным профессором Саарского университета . Его исследовательская группа создала SPASS автоматизированное средство доказательства теорем .

он получил премию Эрбрана В 2004 году ( посмертно ) за важный вклад в автоматизированное доказательство теорем .

Ссылки

• Доказательство теоремы уравнений на основе перезаписи с выбором и упрощением , Лео Бахмайр и Харальд Ганзингер, Журнал логики и вычислений 3 (4), 1994.

Внешние ссылки

• Персональная домашняя страница Харальда Ганцингера — версия от 7 декабря 2013 г., сохранена на archive.org.