Volume 6: January - December 1996

Issue 4: August 1996


An interactive solution to the n x n mutilated checkerboard problem

  • An interactive solution to the n x n mutilated checkerboard problem
  • S. Subramanian Trusted Information Systems, 444 Castro Street, Suite 800, Mountain View, CA 94041, USA. Email: sakthi@ba.tis.com


    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 x 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.

    Keywords: Automated theorem proving, mutilated checkerboard problem, artificial intelligence, finite state machines.

    Pages: 573 - 598

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Last updated 09 Sep 96

    Part of the OUP Journals World Wide Web service.

    Copyright Oxford University Press, 1996