## Abstract

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
ABSTRACT

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