Кузнецов С.Л. Coq: построение и проверка математических доказательств на компьютере ()

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