Из блога Терренса Тао узнал, что есть такая логическая игра QED или по-другому можно назвать интерактивный учебник логики.
Рекомендую всем, кому больше 10 лет и кто интересуется theorem prover-ами.

P.S.
Для игры (и для работы с theorem prover-ами тоже) полезно знакомство с Natural deduction Генцена. К сожалению сейчас не вспомню, где об этом хорошо написано по-русски.

HH> узнал, что есть такая логическая игра QED или по-другому можно назвать интерактивный учебник логики.

Ну скукота же Перекиньте мышкой слева направо — QED!

Здравствуйте, bzig, Вы писали:

B>Ну скукота же Перекиньте мышкой слева направо — QED!

Так это же не развлечение и не пазл, это учебник логики. Хотя там добавлены некоторые развлекательные элементы, например можно попытаться найти самое короткое доказательство, при этом экран становится зеленым, а не синим.
Но главное что есть шанс использовать это для дела. По крайней мере некоторые математики с помощью того же самого*, но записанного на языке Lean theorem prover, доказывают теоремы.
P.S. Если Вам это не интересно, то может быть оно Вам и не надо.
P.P.S. Если точно не знаете надо ли оно Вам, то попробуйте почитать бумаги Wadler или посмотреть его выступление на тему Propositions as Types.

*Если почитать мануал по Lean theorem prover, там используются те же правила introduction — elimination для и-или-следует, затем кванторы "для любого" "существует", которые в теории зависимых типов соответствуют зависимому произведению и зависимой паре, дальше свойства отношений и равенство и т.д.