alogic: (Default)
2011-12-08 03:12 am
Entry tags:

Вопрос по математической логике

Оригинал взят у [livejournal.com profile] ygam в Вопрос по математической логике
Как парадокс Ришара работает с числами, способность описания которых русскими фразами меняется изо дня в день? Фраза "знак уверенности в том, что результаты российских выборов сфальсифицированы" содержит 9 слов. До сегодняшнего дня она ничего не означала, а сегодня стала означать число 632305222316434. Фраза "шестьсот тридцать два триллиона триста пять миллиардов двести двадцать два миллиона триста шестнадцать тысяч четыреста тридцать четыре" содержит 17 слов.
alogic: (Default)
2011-01-21 08:02 pm
Entry tags:

автоматический доказатель

После нового года опять заработал мехматовский семинарчик по логике. Сейчас Женя Беркович на доске программирует в примитивно-рекурсивных функциях лямбда-исчисление. Доказывает, что они эквивалентны. Можно подумать кто-то сомневался. Но есть же любители.

В перерывах между смотрением на доску, скачал книгу Logic in Computer Science 2nd - Huth & Ryan.PDF. Я под впечатлением от открытия для себя изоморфизма Кари-Говарда, автоматического доказателя теорем Coq, а так же созданного с его помощью формально доказанного компилятора Compsert. Жду не дождусь, когда компьютеры заменят программистов.
alogic: (Default)
2009-12-15 04:13 am
Entry tags:

(no subject)

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