Кузнецов С.Л. Coq: построение и проверка математических доказательств на компьютере ()
В докладе дается обзор системы Coq — средства для полуавтоматического построения и автоматической проверки доказательств на компьютере. Возможность формальной проверки доказательств теорем особенна ценна в случаях, когда сложность и объём текста доказательства делает его необозримым для человека. Один из известных примеров (о котором пойдёт речь в докладе) — решение задачи о четырёх красках. Ещё одним (возможно, даже более важным) применением Coq является разработка программных продуктов, корректность работы которых доказана формально и которые предназначены для использования в критических ситуациях (например, управление опасными производствами). Одной из важных специфических черт Coq является возможность извлечения реализации алгоритма в виде программы из формального доказательства его корректности.
Докладчик: Кузнецов Степан Львович, кафедра матем. логики, мехмат МГУ; МИАН; ВШЭ.
Слайды:
====================================
МГУ им. М. В. Ломоносова
Механико-математический факультет
Кафедра математической логики и теории алгоритмов
Научно-исследовательский семинар
по математической логике
под руководством
академика РАН С. И. Адяна,
академика РАН Л. Д. Беклемишева
и академика РАН А. Л. Семёнова
(по средам в ауд. 16-04 ГЗ МГУ)
Веб-страница семинара: