Discussed here. This interface would create a "game" where one has to fill out a multiplication table of a specified size. At any given stage of the game, the table will be partially filled out, and the status of various selected laws will be displayed: "false" (with some explicit values of variables supplied on request), "true" (which would only happen when the table is fully completed), or "undetermined" (where the table is incomplete, but no counterexamples found so far).
A more advanced feature would be to suggest "autocompletes" (in the spirit of "Minesweeper") based on the laws one wants to prove - possibly even incorporating automated theorem provers or SAT solvers natively.
EricGT
commented
2 weeks ago
Discussed here. This interface would create a "game" where one has to fill out a multiplication table of a specified size. At any given stage of the game, the table will be partially filled out, and the status of various selected laws will be displayed: "false" (with some explicit values of variables supplied on request), "true" (which would only happen when the table is fully completed), or "undetermined" (where the table is incomplete, but no counterexamples found so far).
A more advanced feature would be to suggest "autocompletes" (in the spirit of "Minesweeper") based on the laws one wants to prove - possibly even incorporating automated theorem provers or SAT solvers natively.