Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem

There are many papers describing problems solved using the Boyer-Moore theorem prover, as well as papers describing new tools and functionalities added to it. Unfortunately, so far there has been no tutorial paper describing typical interactions that a user has with this system when trying to solve a nontrivial problem, including a discussion of issues that arise in these situations. In this paper we aim to fill this gap by illustrating how we have proved an interesting theorem with the Boyer-Moore theorem prover: a formalization of the assertion that the arithmetic mean of a sequence of natural numbers is greater than or equal to their geometric mean. We hope that this report will be of value not only for (non-expert) users of this system, who can learn some approaches (and tricks) to use when proving theorems with it, but also for implementors of automated deduction systems. Perhaps our main point is that, at least in the case of Nqthm, the user can interact with the system without knowing much about how it works inside. This perspective suggests the development of theorem provers that allow interaction that is user oriented and not system developer oriented. This research was supported in part by ONR Contract N00014-94-C-0193. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Office of Naval Research, or the U.S. government.