An interactive solution to the n x n mutilated checkerboard problem
S Subramanian · Journal of Logic and Computation · 1996
We present a method of modelling parameterized classes of finite state machines in the Boyer-Moore logic so that invariant properties can be verified interactively using the Boyer-Moore theorem prover. We illustrate our approach using an interactive proof of the impossibility of covering an n × n ‘mutilated’ checkerboard completely with dominoes. We model the problem by defining a simulator and formalize the well-known parity argument as a proof by mathematical induction on the length of action sequences executed starting with an empty board. The suitability of our approach for verifying properties depends strongly on the actual Lisp data structures and programs used in the simulation model. We explain some of the choices we made in simplifying the checkerboard problem representation and describe in detail the heuristic guidance given to the theorem prover.