Курс лекций «Автоматическое доказательство теорем»
С 28 сентября Джон Харрисон прочитает серию лекций об автоматическом доказательстве теорем:
Background, history and propositional logic. First-order logic with and without equality. Decidable problems in logic and algebra. Interactive theorem proving and proof-checking. Applications to mathematics and computer verification. Лекции будут проходить в ПОМИ РАН (Санкт-Петербург, наб. р. Фонтанки, 27), Мраморный зал, второй этаж.
Слайды, видеозаписи и другие материалы лекций будут доступны для всех желающих на странице курса.
Клуб открыт абсолютно для всех: вход свободный, лекции бесплатные, никакой предварительной регистрации не требуется.
Профессор Харрисон занимается формальной верификацией в компании Intel Corporation. Его основной специализацией является верификация алгоритмов, работающих с числами с плавающей точкой.
образование, санкт-петербург