Курс лекций «Автоматическое доказательство теорем»

С 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. Его основной специализацией является верификация алгоритмов, работающих с числами с плавающей точкой.

  образование, санкт-петербург

©  Linux.org.ru