LINUX.ORG.RU

Курс лекций «Автоматическое доказательство теорем»

 ,


9

4

С 28 сентября Джон Харрисон прочитает серию лекций об автоматическом доказательстве теорем:

  • Background, history and propositional logic.
  • First-order logic with and without equality.
  • Decidable problems in logic and algebra.
  • Interactive theorem proving and proof-checking.
  • Applications to mathematics and computer verification.

Лекции будут проходить в ПОМИ РАН (Санкт-Петербург, наб. р. Фонтанки, 27), Мраморный зал, второй этаж.

Слайды, видеозаписи и другие материалы лекций будут доступны для всех желающих на странице курса.

Клуб открыт абсолютно для всех: вход свободный, лекции бесплатные, никакой предварительной регистрации не требуется.

Профессор Харрисон занимается формальной верификацией в компании Intel Corporation. Его основной специализацией является верификация алгоритмов, работающих с числами с плавающей точкой.

>>> Подробности

★★★★★

Проверено: Shaman007 ()
Последнее исправление: Shaman007 (всего исправлений: 1)

Ответ на: комментарий от www_linux_org_ru

анализ требований заказчика и составление по нему технического задания — это:

1. research 2. development 3. r&d 4. ни одно из этих

4-ый вариант, процесс управления требованиями. который, если по уму, может включать 2, если все практики отработаны, 3 если не очень, 1 если идея продукта пока ещё только на уровне прототипа.

ы?

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

"интер-универсальный геометр"

ещё, из комментов на хабре про Пенроуза

Ну. Вообще, Пенроуз активно не верит в то, что искусственный интеллект можно создать и объясняет это тем, что человек может решать алгоритмически неразрешимые задачи. У него даже две книги об этом есть. Но в данном случае он говорит именно о том, что разные системы аксиом позволяют получать разные утверждения об одних и тех же объектах. Он потом там о геометриях различных рассуждает.

я вот тут подумал, как можно понять по простому, по быстрому, что такое интер-универсальный геометр (моя версия):

«разные утверждения из разных систем, об одних и тех же объектах. Разные, но универсальные ну или хотя бы интер-универсальные»

есть субъективность, интер-субъективность, и объективность (универсальность)

cубъективное := зависит от субъекта, его точки зрения

объективное := не зависит ни от какого субъекта, только от объекта

интерсубъективное := «почти объективное», которое ещё не проверено и не общепризнано.

универсальное почти то же, что и объективное (но не совсем)

объективность := общепризнанная универсальность вставим перед последними двумя

«интер-универсальность»: непризнанная универсальность,

междисциплинарная универсальность с претензией на общепризнанность, но всё ещё «неэргономичное знание», то, которое сложно понять и проверить

ИМХО, это бы объясняло титул математика и его систему понятий, его язык.

вообще потребуется какое-то декомпилирование метаязыка, его системы понятий, системы правил и выводов на этом языке,

+ оптимизация (перетолмачивание на понятность/когнитивность/эргономичность, и/или, извлечение знаний, математических подходов и инструментов доказательства, ходов)

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

если

а) это яйцеголовое теоретизирование не ограничить, продукта на выходе и не будет

Если это $ANY_MASTURBATION не ограничить, продукта на выходе не будет.

Кстати, Хоар и Вирт, авторы Algol W, оба академики.

tailgunner ★★★★★
()
Последнее исправление: tailgunner (всего исправлений: 1)
Ответ на: комментарий от tailgunner

с другой стороны, если нам так хочется $ANY_MASTURBATION на эвристики, ну кто нас, взрослых людей заставляет делать это руками? есть же, слава роботам, девайсы для этого.

вот например как компьютер сгенерировал эффективные, но непонятные человеку алгоритмы ускорения TCP

или вот это, старое

Томпсон задался вопросом, что получится, если применить метод генетических алгоритмов к электронным схемам. Нужно сформулировать какую-нибудь задачу, случайным образом комбинировать схемы, которые способны или не способны ее решить, отбирать схемы, которые лучше справляются с решением, и повторять процесс в течение стольких поколений, сколько потребуется ... Предположительно. Томпсон описал работу микросхемы так: «На самом деле я не имею ни малейшего понятия о том, как она работает». Дальнейшее исследование окончательного решения выявило еще более удивительный факт: на самом деле использовались только 32 ячейки из 100. Остальные можно было удалить из схемы, никак не повлияв на ее работу. Сначала казалось, что можно удалить еще пять ячеек, которые не были электрически связаны ни с другими ячейками, ни с входом, ни с выходом. Однако после их удаления схема переставала работать. Возможно, эти ячейки реагировали не на электрический ток, а какие-то иные свойства остальных ячеек схемы — например, их магнитное поле. Какова бы ни была причина, интуиция Томпсона была абсолютно верной: у настоящей кремниевой микросхемы припрятано больше козырей в рукаве, чем у ее компьютерной симуляции.

( более нормальное описание эксперимента )

это к тому, что «теории обосрались и не нужны, ибо жалкие 2%, а средненькая эвристика рулед».

ДА, сейчас с устойчивостью проблемы — при каждом изменении каких-то параметров нужно переобучение, и ещё вопрос сколько оно займёт, и ещё вопрос с чувствительностью/устойчивостью на изменение параметров.

но если это делать как-то направлено, адаптивно, а не совсем наобум?

тогда эвристики могут выэволюционировать совсем не средненькие, чем какой-то там быдлокодеришка наговнякает.

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

вот нагрянут массово вот такие например, девайсы

более прикольная ссылка

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