HexProver - Revision history

Selinger: Minor copy-editing.

2024-06-30T19:38:47Z

Minor copy-editing.

Comonoid: add date

2024-06-04T19:18:38Z

add date

Comonoid: Add basic information on mirefek's HexProver

2024-06-04T19:16:03Z

Add basic information on mirefek's HexProver

New page

HexProver is an interactive tool for verifying Hex templates created by user mirefek 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 lemmata. 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.

== External links ==

[https://github.com/mirefek/HexProver GitHub repository]

@@ 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 lemmata. 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.
+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.

← Older revision		Revision as of 19:18, 4 June 2024
Line 1:		Line 1:
−	HexProver is an interactive tool for verifying Hex templates created by user mirefek 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 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 lemmata. 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.		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 lemmata. 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.