Difference between revisions of "HexProver"
m (add date) |
m (Minor copy-editing.) |
||
| Line 1: | Line 1: | ||
| − | HexProver is an interactive tool for verifying Hex templates created by user mirefek in September 2023 and shared on the [[Hex forums|Hex Discord]]. It does not employ brute-force search, instead helping the user to manually prove the validity of a template. | + | HexProver is an interactive tool for verifying Hex templates created by the user mirefek in September 2023 and shared on the [[Hex forums|Hex Discord]]. It does not employ brute-force search, instead helping the user to manually prove the validity of a template. |
| − | The tool allows to "split goals" and verify parts of the template independently. With the "Automation" button enabled, proofs of the subtemplates are automatically reused in a different board configuration (however, as for now, subgoal proofs are not position-independent or symmetry-independent). The proven theorem is saved to a text-based file with the .hpf extension, including the used | + | The tool allows the user to "split goals" and verify parts of the template independently. With the "Automation" button enabled, proofs of the subtemplates are automatically reused in a different board configuration (however, as for now, subgoal proofs are not position-independent or symmetry-independent). The proven theorem is saved to a text-based file with the .hpf extension, including the used lemmas. The template itself is described as an ASCII hexagonal board in the .hdg files. Once a template is fully verified, one can play as the template's intruder and see all the possible responses. |
For further information, consult the project's GitHub page. | For further information, consult the project's GitHub page. | ||
Latest revision as of 19:38, 30 June 2024
HexProver is an interactive tool for verifying Hex templates created by the user mirefek in September 2023 and shared on the Hex Discord. It does not employ brute-force search, instead helping the user to manually prove the validity of a template.
The tool allows the user to "split goals" and verify parts of the template independently. With the "Automation" button enabled, proofs of the subtemplates are automatically reused in a different board configuration (however, as for now, subgoal proofs are not position-independent or symmetry-independent). The proven theorem is saved to a text-based file with the .hpf extension, including the used lemmas. The template itself is described as an ASCII hexagonal board in the .hdg files. Once a template is fully verified, one can play as the template's intruder and see all the possible responses.
For further information, consult the project's GitHub page.
