I made this theory script showing how you can use HOL4 to: *Arrive at a solution of the riddle *Then store a theorem with the solution
The theorem “riddle_solution” informally states that: *The riddle has a solution. *In any solution, the portrait is in the golden box. If you are going to solve a lot of puzzles, it may be worth doing automation. You can define a function that find the solution (if any) and then proves whether the solution is unique and a theorem with an explicit solution given. If you find this example useful please consider donating Bitcoins to 1F6zgVha3QwNqqpa7Wzf7cj52B7eyZSydX to help me with day to day running expenses.
riddleScript.sml
Description: application/smil
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
