Here is a thing I just made. It is implemented in javascript, ugh. I tested it in firefox, ymmv if you use another browser.
I'm interested to see if people totally unfamiliar with logic find it sensible as a game. A big part of it, I suppose, whether you are familiar or not, is figuring out what each color of "bracket" does when you click on it. If you are confused, I recommend fiddling around even with the "easy" puzzles even after you beat them to see what things don't work as well as which things do.
But I've had this notion for a little while to play around with turning ordinary proof search into a little clickety puzzle game like this — sort of a more visual version of the incinerator subpuzzle from CMU's ICFP contest run a couple of years ago — and I'm happy to find that it wasn't so hard. I feel that tableaux-style proof search classical modal logic minimizes the number of interaction concepts in the game, despite my love for constructivism and sequent calculi.
← Ctrl ← Alt
Ctrl → Alt →
← Ctrl ← Alt
Ctrl → Alt →