Кристоф Вальтер

Кристоф Вальтер
Кристоф Вальтер
Рожденный	9 августа 1950 г. (73 года)
Альма-матер	Университет Карлсруэ
Известный	Вальтеровская рекурсия
	Научная карьера
Диссертация	Многосортное исчисление, основанное на разрешении и парамодуляции (1984)
Докторантура	Питер Деуссен

Кристоф Вальтер (родился 9 августа 1950 г.) ^[1]— немецкий учёный-компьютерщик, известный своим вкладом в автоматизированное доказательство теорем .Он является почетным профессором Дармштадтского технологического университета . ^[2]

Избранные публикации

Об автоматизированном доказательстве теорем

Томас Кольбе; Кристоф Вальтер (1994). «Повторное использование доказательств» . В Энтони Коне (ред.). Учеб. 11-й Европейской конф. по искусственному интеллекту (ECAI-11) . Джон Уайли и сыновья. стр. 80–84.
Томас Кольбе; Кристоф Вальтер (1995). «Адаптация доказательств для повторного использования» . Учеб. Осенний симпозиум AAAI 1995 г. по адаптации знаний для повторного использования . Пресса АААИ. стр. 61–67.
Томас Кольбе; Кристоф Вальтер (1995). «Управление и поиск доказательств» . Учеб. IJCAI-14 Семинар по формальным подходам к повторному использованию планов, доказательств и программ . Морган Кауфманн. стр. 1–5.
Томас Кольбе; Кристоф Вальтер (1995). «Оценка соответствия второго порядка по модулю – метод повторного использования доказательств» . Учеб. 14-й стажер. Совместная конф. по искусственному интеллекту (IJCAI-14) . Морган Кауфманн. стр. 190–195.
Томас Кольбе; Кристоф Вальтер (1995). «Исправление доказательств для повторного использования» . Учеб. VIII Европейской конф. по машинному обучению (ECML-8) . ЛНАИ. Том. 912. Спрингер. стр. 303–306.
Томас Кольбе; Кристоф Вальтер (1996). «Завершение доказательства теоремы повторным использованием» . В Массачусетсе МакРобби; Дж. К. Слейни (ред.). Учеб. 13-й Интер. Конф. по автоматическому вычету (CADE-13) . ЛНАИ. Том. 1104. Спрингер. стр. 106–120.
Томас Кольбе; Кристоф Вальтер (1996). «Доказательство теорем, имитируя человеческие навыки» . Весенний симпозиум AAAI 1996 г. по приобретению, обучению и демонстрации . Пресса АААИ. стр. 50–56.
Томас Кольбе; Кристоф Вальтер (1998). «Анализ доказательств, обобщение и повторное использование». У Вольфганга Бибеля ; Питер Шмитт (ред.). Автоматизированный вычет — основа для приложений . Том. 9. Дордрехт: Академическое издательство Kluwer. стр. 189–219. дои : 10.1007/978-94-017-0435-9_8 .
Кристоф Вальтер; Томас Кольбе (2000). «О прекращении леммистских спекуляций» . Информация и вычисления . 162 (1–2): 96–116. дои : 10.1006/inco.1999.2859 .
Кристоф Вальтер; Томас Кольбе (2000). «Доказательство теорем повторным использованием». Искусственный интеллект . 116 (1–2): 17–66. дои : 10.1016/S0004-3702(99)00096-X .
Кристоф Вальтер (2003). «Автоматическое доказательство». В Гюнтере Гёрце (ред.). Введение в искусственный интеллект . Эддисон Уэсли. стр. 223–263.

Об автоматическом анализе терминации

Кристоф Вальтер (1988). «Алгоритмы, ограниченные аргументами, как основа автоматического доказательства завершения». Учеб. 9-я конференция по автоматизированному дедукции . ЛНАИ . Том. 310. Спрингер. стр. 602–621.
Кристоф Вальтер (1991). «Автоматизация расторжения договора» . В Библии Вольфганга (ред.). Искусственный интеллект . Посмотретьег. стр. 1–254.
Кристоф Вальтер (1991). «О доказательстве машинного завершения алгоритмов» . Искусственный интеллект . 70 (1).
Юрген Гизль; Кристоф Вальтер; Юрген Браубургер (1998). «Анализ завершения функциональных программ». У Вольфганга Бибеля ; Питер Шмитт (ред.). Автоматизированный вычет — основа для приложений . Том. 10. Дордрехт: Академическое издательство Kluwer. стр. 135–164. дои : 10.1007/978-94-017-0437-3_6 .
Кристоф Вальтер (2000). «Критерии прекращения». В С. Хёльдоблере (ред.). Интеллектика и вычислительная логика . Дордрехт: Kluwer Academic Publishers. стр. 361–386.
Кристоф Вальтер; Стефан Швейцер (2005). «Автоматизированный анализ завершения неполностью определенных программ» . У Франца Баадера ; Андрей Воронков (ред.). Учеб. 11-й Международный. Конф. по логике программирования, искусственному интеллекту и рассуждению (LPAR) . ЛНАИ. Том. 3452. Спрингер. стр. 332–346.

О VeriFun системе проверки работоспособности программ

Кристоф Вальтер и Стефан Швейцер (2003). «О ВериФун» . У Франца Баадера (ред.). Учеб. 19-я конференция по автоматизированному дедукции . ЛНАИ. Том. 2741. Спрингер. стр. 322–327.
Кристоф Вальтер; Стефан Швейцер (2004). «Проверка на уроке» . Журнал автоматизированного рассуждения . 31 (1): 35–73. дои : 10.1016/0004-3702(85)90029-3 .
Кристоф Вальтер; Стефан Швейцер (2005). «Генератор кода с машинной проверкой» . У Моше Ю. Варди ; Андрей Воронков (ред.). Учеб. 10-й Международный. Конф. по логике программирования, искусственному интеллекту и рассуждению (LPAR-10) . ЛНАИ. Том. 2850. Спрингер. стр. 91–106.
Кристоф Вальтер; Стефан Швейцер (2005). «Рассуждения о неполностью определенных программах» . У Джеффа Сатклиффа ; Андрей Воронков (ред.). Учеб. 12-й Международный. Конф. по логике программирования, искусственному интеллекту и рассуждению (LPAR-12) . ЛНАИ. Том. 3835. Спрингер. стр. 427–442.
Маркус Адерхольд; Кристоф Вальтер; Дэниел Саллис; Андреас Шлоссер (2006). «Быстрое опровержение VeriFun» . У Вольфганга Арендта; Питер Баумгартнер; Ханс де Нивель (ред.). Учеб. Семинар «Не-теоремы, недействительность, недоказуемость» (ОТВЕРЖЕНИЕ-06) . стр. 59–69.
Андреас Шлоссер; Кристоф Вальтер; Маркус Адерхольд (2006). «Аксиоматические спецификации в VeriFun» . У Сержа Отексье; Хайко Мантель (ред.). Учеб. 6-й проверочный семинар (VERIFY-06) . стр. 146–163.
Андреас Шлоссер; Кристоф Вальтер; Майкл Гондер; Маркус Адерхольд (2007). «Контекстно-зависимые процедуры и вычисляемые типы в VeriFun» . Электронные заметки по теоретической информатике . 174 (7): 61–78. дои : 10.1016/j.entcs.2006.10.038 .
Кристоф Вальтер; Натан Вассер (2017). «Ферма, Эйлер, Вильсон - три примера теории чисел» . Журнал автоматизированного рассуждения . 59 (2): 267–286. дои : 10.1007/s10817-016-9387-z .
Кристоф Вальтер (2018). «Формально проверенное умножение Монтгомери» . В Хане Чоклер; Георг Вайсенбахер (ред.). Учеб. 30-го интерна. Конф. по компьютерной верификации (CAV 2018) . ЛНАИ. Том. 10982. Спрингер. стр. 505–522. дои : 10.1007/978-3-319-96142-2_30 .
Кристоф Вальтер (2019). «Проверенная итерация Ньютона-Рафсона для мультипликативных обратных операций по модулю степени любого основания» . Транзакции ACM в математическом программном обеспечении (TOMS) . 45 (1): 9:1–9:7. дои : 10.1145/3301317 .

О многообразном объединении, разрешении и парамодуляции

Кристоф Вальтер (1983). «Множественное исчисление, основанное на разрешении и парамодуляции». У Алана Банди (ред.). Учеб. 8-го интерна. Совместная конф. по искусственному интеллекту (IJCAI-8) . Морган Кауфманн. стр. 882–891.
Кристоф Вальтер (1984). «Механическое решение парового катка Шуберта с помощью многосортного разрешения». Учеб. 4-й Национальной конф. по искусственному интеллекту (AAAI-4) . Морган Кауфманн. стр. 330–334.
Кристоф Вальтер (1984). «Объединение в многосортных теориях». В Тиме О'Ши (ред.). Учеб. VI Европейской конференции. по искусственному интеллекту (ECAI-6) . Северная Голландия. стр. 383–392.
Вальтер, Кристоф (1985). «Механическое решение парового катка Шуберта с помощью многосортного разрешения». Артиф. Интелл . 26 (2): 217–224. дои : 10.1016/0004-3702(85)90029-3 .
Кристоф Вальтер (1986). «Классификация многосортных проблем унификации». В Йорге Зикманне (ред.). Учеб. 8-го Интера. Конф. по автоматическому вычету (CADE-8) . ЛНАИ. Том. 230. Спрингер. стр. 525–537.
Кристоф Вальтер (1987). Многосортное исчисление, основанное на разрешении и парамодуляции . Питман (Лондон) и Морган Кауфманн (Лос-Альтос). стр. 1–170.
Кристоф Вальтер (1988). «Многосортовое объединение». Дж. АКМ . 35 (1): 1–17. дои : 10.1145/42267.45071 .
Кристоф Вальтер (1990). «Множественные выводы в автоматизированном доказательстве теорем». В К.-Х. Блазиус; У. Хедтштюк; К.-Р. Роллингер (ред.). Сортировки и типы в искусственном интеллекте . ЛНАИ. Том. 418. Спрингер. стр. 18–48.
Кристоф Вальтер (2016). Алгоритм многосортной унификации (Ошибки в многосортированной унификации, J. ACM, том 35 (1), 1988) (Технический отчет). ТУ Дармштадт.

Об индукционном доказательстве

Сюзанна Бюндо , Биргит Хаммель, Дитер Хуттер и Кристоф Вальтер (1986). «Система доказательства индукционных теорем Карлсруэ». В JH Siekmann (ред.). Учеб. 8-й КАДЕ . ЛНАИ. Том. 230. Спрингер. стр. 672–674.
Кристоф Вальтер (1992). «Математическая индукция» . В СК Шапиро (ред.). Энциклопедия искусственного интеллекта . Джон Уайли и сыновья. стр. 668–672.
Кристоф Вальтер (1992). «Вычисление аксиом индукции» (PDF) . У Андрея Воронкова (ред.). Учеб. ЛПАР . ЛНАИ. Том. 624. Спрингер. стр. 381–392.
Кристоф Вальтер (1993). «Машинное объединение аксиом индукции» (PDF) . В Ружене Байчи (ред.). Учеб. 13-й IJCAI . Морган Кауфманн. стр. 95–101.
Кристоф Вальтер (1994). «Математическая индукция» (PDF) . В Дов М. Габбай , С. Дж. Хоггер и Дж. А. Робинсон (ред.). Справочник по логике в искусственном интеллекте и логическом программировании . Том. 2. Издательство Оксфордского университета. стр. 127–227.
Кристоф Вальтер (2001). «Семантика и верификация программ» . Тексты Тойбнера по информатике . Том 34. Тойбнер-Вили. стр. 1–212.

Ссылки

^ Саймон Зиглер и Натан Вассер, изд. (2010). "Предисловие". Проверка, индукция, анализ завершения — Праздничная грамота Кристофа Вальтера по случаю его 60-летия . ЛНАИ . Том. 6463. Спрингер. ISBN 978-3-642-17171-0 .
↑ Профессора и руководители групп . Архивировано 21 февраля 2015 г. в Wayback Machine (секция почетных профессоров и профессоров на пенсии ) на веб-сайте Дармштадтского университета.

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

Домашняя страница Кристофа Вальтера в Дармштадтском университете
Система VeriFun в Дармштадтском университете

[1] Саймон Зиглер и Натан Вассер, изд. (2010). "Предисловие". Проверка, индукция, анализ завершения — Праздничная грамота Кристофа Вальтера по случаю его 60-летия . ЛНАИ . Том. 6463. Спрингер. ISBN 978-3-642-17171-0 .

[2] Профессора и руководители групп . Архивировано 21 февраля 2015 г. в Wayback Machine (секция почетных профессоров и профессоров на пенсии ) на веб-сайте Дармштадтского университета.

[1]

[2]

Базы данных авторитетного контроля
Международный	БЫСТРЫЙ ЯВЛЯЮТСЯ ВИАФ WorldCat
Национальный	Германия Израиль Соединенные Штаты
академики	ДБЛП MathSciNet Проект математической генеалогии
Другой	ИдРеф