S. Subramanian Trusted Information Systems, 444 Castro Street, Suite 800, Mountain View, CA 94041, USA. Email: email@example.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
nx 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. : Automated theorem proving, mutilated checkerboard problem, artificial intelligence, finite state machines.
Part of the OUP Journal of Logic and Computation WWW service
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