Из
блога Терренса Тао узнал, что есть такая логическая игра
QED или по-другому можно назвать интерактивный учебник логики.
Рекомендую всем, кому больше 10 лет и кто интересуется theorem prover-ами.
P.S.
Для игры (и для работы с theorem prover-ами тоже) полезно знакомство с
Natural deduction Генцена. К сожалению сейчас не вспомню, где об этом хорошо написано по-русски.
Здравствуйте, bzig, Вы писали:
B>Ну скукота же Перекиньте мышкой слева направо — QED!
Так это же не развлечение и не пазл, это учебник логики. Хотя там добавлены некоторые развлекательные элементы, например можно попытаться найти самое короткое доказательство, при этом экран становится зеленым, а не синим.
Но главное что есть шанс использовать это для дела. По крайней мере некоторые математики с помощью того же самого*, но записанного на языке Lean theorem prover,
доказывают теоремы.
P.S. Если Вам это не интересно, то может быть оно Вам и не надо.
P.P.S. Если точно не знаете надо ли оно Вам, то попробуйте почитать
бумаги Wadler или посмотреть его выступление на тему Propositions as Types.
*Если почитать
мануал по Lean theorem prover, там используются те же правила introduction — elimination для и-или-следует, затем кванторы "для любого" "существует", которые в теории зависимых типов соответствуют зависимому произведению и зависимой паре, дальше свойства отношений и равенство и т.д.
HH> узнал, что есть такая логическая игра QED или по-другому можно назвать интерактивный учебник логики.
Ну скукота же
Перекиньте мышкой слева направо — QED!