A Fascinating Country in the World of Computing

Rating:
Summary: unconventional, but effective
Review: When reading one of Larry Wos' books one is often surprised to find a complete lack of rigor when discussing a topic such as automated reasoning that is usually made extremely rigorous by the computer scientists, logicians, and mathematicians who have developed the subject over the past 50 years. At first my reaction to this was one of disappointment and disbelief (i.e. where's the beef?); but then I quickly began to realize that this book may end up being one of the most influential I've ever read, for the simple reason that it is written by a man who clearly loves the subject and has both inspired me and made it quite convenient (by including the source code for Otter and emphasizing the language Otter understands throughout the book) for me to begin my journey through the fascinating country. Indeed, unlike most academic authors who fear their reputation will suffer if they write on anything that does not require scores of new symbols, Larry seems to be saying that it is not about the book and its ideas, but more about Otter and an invitation to explore a vast new world that experimenting with Otter represents. To accomplish this, the only new symbolism you will see in this book is that needed to create an input file for Otter to process. Thus, Larry's approach is quite hands-on/empirical rather than theoretical. With that said, I think this book is ideal for anyone who has formally studied automated reasoning and is ready to experiement with an automated-reasoning program, such as Otter, whose code is supplied on the CD Rom accompanying the book. I myself had spent the latter half of 2000 pouring through Jean Gallier's "Logic For Computer Science: An Introduction to Automated Theorem Proving", and it was from reading this that I became interested in the field. Had I not read that text, I do not think I would have been prepared to fully understand what Larry was trying to convey, especially in Chapter 3: Automated Reasoning in Full. Thus if you have little or no experience with logic and automated deduction systems, I suggest supplementing this text with either Nissanke's logic text, Ben Ari's, or any introductory book that explains resolution and unification in full (Gallier's book I consider an academic masterpiece, but it is also a graduate text and hence contains *much* more than you really need). Personally, I believe that anyone who makes significant contributions to this field in the future will do so using a combination of theory and experimentation. Moreover, if you are thinking of playing with Otter out of curiosity of how it will solve your favorite puzzle, you will not appreciate the solution (proof) nearly as much if you had some formal exposure to logic behind you. Best wishes, and happy experimenting!