LINUX.ORG.RU

Tech Talks @NSU — Автоматическое доказательство теорем

 ,


1

1

Всем привет!

На следующей неделе у нас лекция для математиков и им сочувствующих.

18 ноября, 19:30: Автоматическое доказательство теорем (Ренат Идрисов, к.ф.-м.н., ИСИ СО РАН)

«Вы наверняка слышали, что в последнее время далеко не все теоремы доказываются вручную (вот, например, автоматизированный вывод свойств вероятностных алгоритмов, а вот полностью автоматическое доказательство всем известной теоремы о четырех красках).

Как именно работают системы автоматических доказательств и что за языки лежат в их основе? Похоже ли построение автоматических доказательств на программирование? Могу ли я доказывать свои любимые теоремы на C или C++?

В рамках лекции прозвучат ответы на эти и другие вопросы, а также будет проведен небольшой вводный инструктаж по Coq

Лекция пройдет в аудитории 223 нового спорткомплекса НГУ, вход свободный.

Онлайн-трансляция будет доступна вот тут: https://plus.google.com/events/cdtakpptlcidhk43o2sq7se3pqo

Все подробности, как всегда, на http://techtalks.nsu.ru

★★★★★

+1 В смысле за новость. Ренат адекватный спец.

Evgueni ★★★★★ ()

а вот полностью автоматическое доказательство всем известной теоремы о четырех красках

Ну это неправда. Само доказательство полностью «ручное», никакой автоматики там нету.

anonymous ()
Ответ на: комментарий от buddhist

Он бы еще Эпиграмовым назвался.

anonymous ()
Ответ на: комментарий от anonymous

Ну да, заголовок вранье. Надо «автоматическая верификация доказаткльств».

anonymous ()
Ответ на: комментарий от anonymous

Само доказательство полностью «ручное»

я бы согласился, если бы не слово «полностью». автоматика там, конечно же, есть - тактики, свободные объекты. даже Agda не «полностью» ручная

jtootf ★★★★★ ()

Хорошее название, люди поведутся. Помнится, студентом пришел я послушать семинар о «семантике возможных миров». Тоска зеленая, но без обмана.

Deleted ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.