Автоматическое доказательство теорем

28-29 сентября в рамках Computer Science клуба Джон Харрисон (Intel) прочтёт мини-курс "Автоматическое доказательство теорем". О ЛЕКТОРЕ Профессор Харрисон занимается формальной верификацией в компании Intel Corporation. Его основной специализацией является верификация алгоритмов, работающих с числами с плавающей точкой. Профессор Харрисон внёс вклад в разработку стандарта IEEE 754. Является автором книги "Handbook of Practical Logic and Automated Reasoning", а также членом редколлегии журнала Journal of Automated Reasoning. Введение в функциональное программирование (перевод на русский заметок курса): https://code.google.com/p/funprog-ru/downloads/list Домашняя страница: http://www.cl.cam.ac.uk/~jrh13/ КРАТКАЯ АННОТАЦИЯ КУРСА In these lectures I will give a general overview of automated theorem proving in the broad sense, including fully automated methods, interactive methods and their applications in both mathematics and computing. The content of the course will be quite strongly influenced by my book http://www.cambridge.org/9780521899574 and its associated code, but will be more high-level and include more discussion of applications. ПОДРОБНЕЕ http://compsciclub.ru/courses/theoremproving