Michael J. C. Gordon: PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs 2002: 214-229