Soundness Proofs
We have validated our puzzle solving algorithms using the Twelf metatheorem 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:
 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.
 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').
 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'.
 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.
 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.
 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 type0 puzzles are solvable.


A ZIP file containing the complete proof that type1 puzzles are solvable.

Last update:
December 4^{th}, 2008.