OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation
Journal of Logic and Computation
Volume 13, Issue 4, June 2003: pp. 581-594
A Complete Axiomatization for Blocks World
Stephen A. Cook and Yongmei Liu
1Department of Computer Science, University of Toronto, Toronto, ON, Canada M5S 3G4. E-mail: email@example.com, firstname.lastname@example.org
Blocks World (BW) has been one of the most popular model domains in AI history. However, there has not been serious work on axiomatizing the state constraints of BW and giving justification for its soundness and completeness. In this paper, we model a state of BW by a finite collection of finite chains, and call the theory of all these structures BW theory. We present seven simple axioms and prove that their consequences are precisely BW theory, using Ehrenfeucht-Fraïssé games. We give a simple decision procedure for the theory which can be implemented in exponential space, and prove that every decision procedure (even if nondeterministic) for the theory must take at least exponential time. We also give a characterization of all nonstandard models for the theory. Finally, we present an expansion of BW theory and show that it admits elimination of quantifiers. As a result, we are able to characterize all definable predicates in BW theory, and give simple examples of undefinable predicates.
Keywords: Blocks World, finite axiomatization, Ehrenfeucht-Fraïssé games, complexity of logical theories, definable predicates.
Table of Contents
Full-Text PDF (152 KB)