Soundness Proofs

We have validated our puzzle solving algorithms using the Twelf meta-theorem prover.

We represent a puzzle as a tuple (B, P), where B is the puzzle board, and P is the collection of puzzle pieces. A puzzle solving program consists on a list of statements, where each statement shows how to fill a particular pattern in the puzzle. Each time a statement is applied, we remove one area of the puzzle board, plus a number of pieces. To show that a puzzle solving program is correct, we prove the following lemmas:

1. Preservation: If (B, P) is a solvable puzzle, and our puzzle solving program takes a step producing a new puzzle (B', P'), then (B', P') is solvable.
2. Progress: If (B, P) is a solvable puzzle, then our puzzle solving program contains a rule that changes (B, P) into a new puzzle (B', P').
3. Termination: If our puzzle solving program take any step on a puzzle (B, P), producing a new puzzle (B', P'), then B contains one more area than B'.
4. Inversion: If (B', P') is a solvable puzzle, and there is a puzzle (B, P) such that our puzzle solving program takes a step changing (B, P) into (B', P'), then (B, P) is solvable.
5. Correctness (necessity): If P is a solvable puzzle, and its board has N areas, then our puzzle solving program produces a sequence of N statements that remove all the areas from P.
6. Correctness (sufficiency): If our puzzle solving program produces a sequence of N statements that removes all the areas of a puzzle P, then P is solvable.

	A ZIP file containing the complete proof that type-0 puzzles are solvable.
	A ZIP file containing the complete proof that type-1 puzzles are solvable.