Proof Goals - Bram-Hub/LEGUP GitHub Wiki
As LEGUP is intended to help teach formal logic proofs, it should include some proof condition, such as "prove that a solution exists" or "prove that the cell at (1, 1) must be white".
Proof Goal
There are currently 6 different goals:
- Prove the board is solvable
- Prove the board is unsolvable
- Prove the cell(s) at a given location must be of one specified type
- Prove the cell(s) at a given location might be a different type than specified
- Prove the cell(s) has a specific value
- Prove the cell(s) can have multiple values
All of these should apply to every puzzle type. The first two are the default goal, which is typically unnecessary to explain.
The Proof conditions for specific cells can be visualized as a 2x2 grid
| Given Type | Unspecified Type | |
|---|---|---|
| One Value | Goal 3 | Goal 5 |
| Multiple Values | Goal 4 | Goal 6 |