| RUS ENG |
| Полная версия |
|
|
|
| СЕМИНАРЫ |
|
Рабочий семинар по математической логике
|
|||
|
|
|||
|
Верифицированное вычисление асимптотик вещественных функций — 1 В. А. Нестеров Московский физико-технический институт (национальный исследовательский университет), Московская облаcть, г. Долгопрудный |
|||
|
Аннотация: Вычисление асимптотик функций — одна из нетривиальных математических задач, которая однако под силу компьютеру. Исследования в этом направлении были начаты Г. Харди, и доведены до практического алгоритма Дж. Шекеллом в 1990 году. В докладе я расскажу о своей имплементации алгоритма Шекелла (с некоторыми модификациями) в системе интерактивных доказательств Lean. Системы доказательств дают возможность писать доказательства на формальном языке с последующей автоматической проверкой компьютером. В своей работе я имплементировал алгоритм в виде так называемой «тактики» — программы, которая не только возвращает результат (например, предел функции на бесконечности), но и формальное доказательство его корректности (например, того, что функция действительно стремится к найденному значению). Такая тактика, будучи использованной как подпрограмма, позволяет сократить формальные доказательства других результатов в анализе и комбинаторике. |
|||