A Fascinating Country in the World of Computing [Hardcover]

Larry Wos (Author), Gail W. Pieper (Author)

Book Description

ISBN-10: 9810239106 | ISBN-13: 978-9810239107 | Publication Date: March 15, 2000

This text demonstrates - through examples and puzzles and intriguing questions - how to make your computer reason logically. To help you, the book includes a CD-ROM with OTTER, the world's most powerful general-purpose reasoning program. The automation of reasoning has advanced markedly in the last few decades of the 20th century, and this book discusses some of the remarkable successes that automated reasoning programs have had in tackling challenging problems in mathematics, logic, program verification and circuit design. Because the intended audience includes students and teachers, the book provides many exercises (with hints and answers), as well as tutorial chapters that gently introduce readers to the field of logic and to automated reasoning in general. For more advanced researchers, the book presents challenging questions, many of which are still unsolved.

Product Details

• Hardcover: 587 pages
• Publisher: World Scientific Pub Co Inc (March 15, 2000)
• Language: English
• ISBN-10: 9810239106
• ISBN-13: 978-9810239107
• Product Dimensions: 8.8 x 6.4 x 1.5 inches
• Shipping Weight: 2.2 pounds (View shipping rates and policies)
• Average Customer Review: 4.0 out of 5 stars  See all reviews (1 customer review)
• Amazon Best Sellers Rank: #2,505,495 in Books (See Top 100 in Books)

Customer Reviews

Most Helpful Customer Reviews

5 of 5 people found the following review helpful:

4.0 out of 5 stars unconventional, but effective, April 25, 2001

By 

Todd Ebert (Long Beach California) - See all my reviews

This review is from: A Fascinating Country in the World of Computing (Hardcover)

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!