#матлог #учёба #спецсеминар

Семинар «Вероятностные и субструктурные логические системы» (www.mathnet.ru/conf2533) под руководством С.Л. Кузнецова (homepage.mi-ras.ru/~sk/) и С.О. Сперанского (homepage.mi-ras.ru/~speranski/).

Время: 30 октября (четверг), 16:00
Место: МИАН, ауд. 530 + Контур.Толк
 
В.А. Нестеров (МФТИ)
 
Название:
Верифицированное вычисление асимптотик вещественных функций (продолжение)
 
Аннотация:
Вычисление асимптотик функций - одна из нетривиальных математических задач, которая однако под силу компьютеру. Исследования в этом направлении были начаты Г. Харди и доведены до практического алгоритма Дж. Шекеллом в 1990 году.
 
В докладе я расскажу о своей имплементации алгоритма Шекелла (с некоторыми модификациями) в системе интерактивных доказательств Lean. Системы доказательств дают возможность писать доказательства на формальном языке с последующей автоматической проверкой компьютером. В своей работе я имплементировал алгоритм в виде так называемой тактики - программы, которая не только возвращает результат (например, предел функции на бесконечности), но и формальное доказательство его корректности (например, того, что функция действительно стремится к найденному значению). Такая тактика, будучи использованной как подпрограмма, позволяет сократить формальные доказательства других результатов в анализе и комбинаторике.
 
Если планируете посетить заседание (очно или онлайн через Контур.Толк), пожалуйста, зарегистрируйтесь по ссылке в верхней части страницы семинара:
 
https://www.mathnet.ru/conf2533

➰ ВК