3 ms·
Also, has anyone tried building a puzzle game using a proof assistant?
by worldsayshi 4y ago
Also, has anyone tried building a puzzle game using a proof assistant?
- gmfawcett 4y agoI'm pretty sure that Coq is a puzzle game itself, masquerading as a proof assistant!
- schoen 4y agoI've used Z3 to create some logic puzzles, but I was using the SAT solver features rather than the proof features. One effective, if naive, approach to determining whether a logic puzzle has a unique solution is checking: * is my current constraint set satisfiable? * if so, exhibit a satisfying assignment ("foo") * add a new constraint that explicitly excludes the solution "foo" * is the resulting constraint set satisfiable? * if not, great! (the solution "foo" is unique)
- abecedarius 4y agohttps://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... You could go further towards it feeling like a game, yes -- I've been wanting that too. I'm still learning the basics of these things.
- schoen 4y agoBefore playing the Natural Number Game, I played the Incredible Proof Machine: http://incredible.pm/ http://incredible.pm/ It's fun! Admittedly the diagrams tend to explode in size for complicated proofs.