RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Ближайшие семинары
Календарь семинаров
Список семинаров
Архив по годам
Регистрация семинара

Поиск
RSS
Ближайшие семинары





Для просмотра файлов Вам могут потребоваться








Общеинститутский семинар «Коллоквиум МИАН»
5 декабря 2013 г. 16:00, г. Москва, конференц-зал МИАН (ул. Губкина, 8)
 


Доказуемо рекурсивные функции

Л. Д. Беклемишев
Видеозаписи:
Flash Video 692.6 Mb
Flash Video 4,150.0 Mb
MP4 692.6 Mb

Количество просмотров:
Эта страница:1017
Видеофайлы:369
Youtube Video:

Л. Д. Беклемишев
Фотогалерея


Видео не загружается в Ваш браузер:
  1. Установите Adobe Flash Player    

  2. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  3. Сообщите администратору портала о данной ошибке



Аннотация: Вычислимая функция $f\colon N\to N$ называется доказуемо рекурсивной в данной формальной теории $T$, если существует алгоритм её вычисления такой, что в $T$ можно доказать утверждение «для любого $x$ существует $y$ такой, что $f(x)=y$». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. Разработка методов верификации программ — важный раздел Computer Science. С другой стороны, мы можем использовать доказуемо рекурсивные функции для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к изучению функций, имеющих катастрофически большой рост и наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений.

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2018