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

Немецкий учёный-компьютерщик (родился в 1950 году)

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

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

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

• Томас Кольбе; Кристоф Вальтер (1994). «Повторное использование доказательств». В Энтони Коне (ред.). Труды 11-й Европейской конференции по искусственному интеллекту (ECAI-11) . John Wiley and Sons. стр. 80–84.
• Томас Кольбе; Кристоф Вальтер (1995). «Адаптация доказательств для повторного использования». Труды осеннего симпозиума AAAI 1995 года по адаптации знаний для повторного использования . Издательство AAAI. С. 61–67.
• Томас Кольбе; Кристоф Вальтер (1995). «Управление доказательствами и их поиск». Труды IJCAI- 14 Семинар по формальным подходам к повторному использованию планов, доказательств и программ . Морган Кауфманн. С. 1–5.
• Томас Кольбе; Кристоф Вальтер (1995). «Оценка модуля соответствия второго порядка – метод повторного использования доказательств». Труды 14-й Международной совместной конференции по искусственному интеллекту (IJCAI-14) . Морган Кауфманн. С. 190–195.
• Томас Кольбе; Кристоф Вальтер (1995). «Исправление доказательств для повторного использования». Труды 8-й Европейской конференции по машинному обучению (ECML-8) . LNAI. Том 912. Springer. С. 303–306. doi :10.1007/3-540-59286-5_73.
• Thomas Kolbe; Christoph Walther (1996). "Завершение доказательства теорем повторным использованием". В MA McRobbie; JK Slaney (ред.). Proc. 13th Inter. Conf. on Automated Deduction (CADE-13) . LNAI. Vol. 1104. Springer. pp. 106–120. doi :10.1007/3-540-61511-3_72. ISBN 978-3-540-61511-8.
• Томас Кольбе; Кристоф Вальтер (1996). «Доказательство теорем путем имитации человеческого мастерства». Весенний симпозиум AAAI 1996 года по приобретению знаний, обучению и демонстрации . Издательство AAAI. С. 50–56.
• Thomas Kolbe; Christoph Walther (1998). "Анализ доказательств, обобщение и повторное использование". В Wolfgang Bibel ; Peter Schmitt (ред.). Автоматизированная дедукция - основа для приложений. Серия Applied Logic. Том 9. Дордрехт: Kluwer Academic Publishers. стр. 189–219. doi :10.1007/978-94-017-0435-9_8. ISBN 978-90-481-5051-9.
• Кристоф Вальтер; Томас Кольбе (2000). «О прекращении леммических спекуляций». Информация и вычисления . 162 (1–2): 96–116. doi : 10.1006/inco.1999.2859 .
• Кристоф Вальтер; Томас Кольбе (2000). «Доказательство теорем повторным использованием». Искусственный интеллект . 116 (1–2): 17–66. doi :10.1016/S0004-3702(99)00096-X.
• Кристоф Вальтер (2003). «Автоматы Beweisen». В Гюнтере Гёрце (ред.). Einführung in die Künstliche Intelligenz . Аддисон-Уэсли. стр. 223–263.

На автоматизированноманализ прекращения

• Кристоф Вальтер (1988). «Алгоритмы с ограниченными аргументами как основа для автоматизированных доказательств завершения». Труды 9-й конференции по автоматизированной дедукции . LNAI . Т. 310. Springer. С. 602–621.
• Кристоф Вальтер (1991). «Автоматизация терминалов». У Вольфганга Бибеля (ред.). Künstliche Intelligenz . Посмотретьег. стр. 1–254. дои : 10.1007/978-3-322-85404-9. ISBN 978-3-528-04771-9.
• Кристоф Вальтер (1991). «О доказательстве завершения алгоритмов машиной». Искусственный интеллект . 70 (1).
• Юрген Гисль; Кристоф Вальтер; Юрген Браубургер (1998). «Анализ завершения для функциональных программ». В Вольфганге Бибеле ; Петере Шмитте (ред.). Автоматизированная дедукция — основа для приложений. Серия «Прикладная логика». Т. 10. Дордрехт: Kluwer Academic Publishers. С. 135–164. doi :10.1007/978-94-017-0437-3_6. ISBN 978-90-481-5052-6.
• Кристоф Вальтер (2000). «Критерии завершения». В S. Hölldobler (ред.). Intellectics and Computational Logic. Дордрехт: Kluwer Academic Publishers. стр. 361–386.
• Кристоф Вальтер; Стефан Швейцер (2005). «Автоматизированный анализ завершения не полностью определенных программ». В Franz Baader ; Андрей Воронков (ред.). Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) . LNAI. Vol. 3452. Springer. pp. 332–346.

НаВериФунсистема проверки функциональных программ

• Кристоф Вальтер и Стефан Швейцер (2003). «О VeriFun». В книге Франца Баадера (ред.). Труды 19-й конференции по автоматизированной дедукции . LNAI. Том 2741. Springer. С. 322–327.
• Кристоф Вальтер; Стефан Швейцер (2004). «Проверка в классе». Журнал автоматизированного рассуждения . 31 (1): 35–73. doi :10.1016/0004-3702(85)90029-3.
• Кристоф Вальтер; Стефан Швейцер (2005). «Генератор машинно-проверенного кода». В Моше И. Варди ; Андрей Воронков (ред.). Труды 10-й Международной конференции по логике для программирования, искусственного интеллекта и рассуждений (LPAR-10) . LNAI. Том 2850. Springer. С. 91–106.
• Кристоф Вальтер; Стефан Швейцер (2005). «Рассуждения о неполных программах». В Geoff Sutcliffe ; Андрей Воронков (ред.). Proc. 12th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-12) . LNAI. Vol. 3835. Springer. pp. 427–442.
• Маркус Адерхольд; Кристоф Вальтер; Дэниел Саллис; Андреас Шлоссер (2006). «Быстрое опровержение VeriFun». У Вольфганга Арендта; Питер Баумгартнер; Ханс де Нивель (ред.). Учеб. Семинар «Не-теоремы, недействительность, недоказуемость» (ОТВЕРЖЕНИЕ-06) . стр. 59–69.
• Андреас Шлоссер; Кристоф Вальтер; Маркус Адерхольд (2006). «Аксиоматические спецификации в VeriFun». В Serge Autexier; Heiko Mantel (ред.). Proc. 6th Verification Workshop (VERIFY-06) . стр. 146–163.
• Андреас Шлоссер; Кристоф Вальтер; Михаэль Гондер; Маркус Адерхольд (2007). «Контекстно-зависимые процедуры и вычисляемые типы в VeriFun». Электронные заметки по теоретической информатике . 174 (7): 61–78. doi :10.1016/j.entcs.2006.10.038.
• Кристоф Вальтер; Натан Вассер (2017). «Ферма, Эйлер, Вильсон — три примера из теории чисел». Журнал автоматизированного рассуждения . 59 (2): 267–286. doi :10.1007/s10817-016-9387-z.
• Кристоф Вальтер (2018). «Формально проверенное умножение Монтгомери». В Hana Chockler; Georg Weissenbacher (ред.). Proc. of the 30th Intern. Conf. on Computer Aided Verification (CAV 2018) . LNAI. Vol. 10982. Springer. pp. 505–522. doi :10.1007/978-3-319-96142-2_30. ISBN 978-3-319-96141-5.
• Кристоф Вальтер (2019). «Проверенная итерация Ньютона-Рафсона для мультипликативных обратных по модулю степеней любого основания». Труды ACM по математическому программному обеспечению . 45 (1): 9:1–9:7. doi :10.1145/3301317.

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

• Кристоф Вальтер (1983). «Многосортное исчисление на основе разрешения и парамодуляции». В Alan Bundy (ред.). Proc. of the 8th Intern. Joint Conf. on Artificial Intelligence (IJCAI-8) . Morgan Kaufmann. стр. 882–891.
• Кристоф Вальтер (1984). «Механическое решение парового катка Шуберта с помощью многосортного разрешения». Труды 4-й Национальной конференции по искусственному интеллекту (AAAI-4) . Морган Кауфманн. С. 330–334.
• Кристоф Вальтер (1984). «Унификация во многих теориях». В Тиме О'Ши (ред.). Труды 6-й Европейской конференции по искусственному интеллекту (ECAI-6) . Северная Голландия. С. 383–392.
• Вальтер, Кристоф (1985). «Механическое решение парового катка Шуберта с помощью многосортного разрешения». Artif. Intell . 26 (2): 217–224. doi :10.1016/0004-3702(85)90029-3.
• Кристоф Вальтер (1986). «Классификация многосортных проблем объединения». В Jörg Siekmann (ред.). Proc. of the 8th Inter. Conf. on Automated Deduction (CADE-8) . LNAI. Vol. 230. Springer. pp. 525–537.
• Кристоф Вальтер (1987). Многосортное исчисление, основанное на разрешении и парамодуляции. Питман (Лондон) и Морган Кауфман (Лос-Альтос). С. 1–170. ISBN 978-0-273-08718-2.
• Кристоф Вальтер (1988). «Многосортное объединение». J. ACM . 35 (1): 1–17. doi :10.1145/42267.45071.
• Кристоф Вальтер (1990). «Многосортные выводы в автоматическом доказательстве теорем». В К.-Х. Блазиус; У. Хедтштюк; К.-Р. Роллингер (ред.). Сорта и типы в искусственном интеллекте . LNAI. Т. 418. Springer. С. 18–48.
• Кристоф Вальтер (2016). Алгоритм для многосортного объединения (Errata to Many-Sorted Unification, J. ACM vol 35(1), 1988) (Технический отчет). Технический университет Дармштадта.

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

• Сюзанна Бьюндо и Биргит Хаммель и Дитер Хуттер и Кристоф Вальтер (1986). «Система доказательства индукционных теорем Карлсруэ». В JH Siekmann (ред.). Proc. 8th CADE . LNAI. Том 230. Springer. стр. 672–674.
• Кристоф Вальтер (1992). «Математическая индукция». В SC Shapiro (ред.). Энциклопедия искусственного интеллекта . John Wiley and Sons. стр. 668–672.
• Кристоф Вальтер (1992). «Вычисление аксиом индукции» (PDF) . У Андрея Воронкова (ред.). Учеб. ЛПАР . ЛНАИ. Том. 624. Спрингер. стр. 381–392.
• Кристоф Вальтер (1993). «Машинное объединение аксиом индукции» (PDF) . В Ружене Байчи (ред.). Учеб. 13-й IJCAI . Морган Кауфманн. стр. 95–101.
• Кристоф Вальтер (1994). «Математическая индукция» (PDF) . В Дов М. Габбее и К. Дж. Хоггере и Дж. А. Робинсоне (ред.). Справочник по логике в искусственном интеллекте и логическом программировании . Том 2. Oxford University Press. С. 127–227.
• Кристоф Вальтер (2001). «Семантика и проверка программ». Тойбнер Текст для информатики . TEUBNER-TEXTE для информатики. Том. 34. Тойбнер-Вили. стр. 1–212. дои : 10.1007/978-3-322-86768-1. ISBN 978-3-519-00336-6.

Ссылки

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

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

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