Customer Reviews

Automated Reasoning and the Discovery of Missing and Elegant Proofs

5 star:		(1)
4 star:		(0)
3 star:		(0)
2 star:		(0)
1 star:		(0)

 

 

In this enthusiastic survey of automated reasoning, Larry Wos -- perhaps the most influential pioneer of the field -- offers a uniquely informative (and entertaining) perspective on some of the major successes in this exciting research area.

Automated reasoning (an outgrowth of automated theorem-proving and artificial intelligence) has gone mainstream and is now contributing a stead stream of new theorems and results to the broader mathematica, scientific, and logical community. The majority of these results have come from Argonne National Laboratory and the research of Larry Wos and his colleague William McCune, the developer of the marvelous reasoning program OTTER, which is featured in this book (and is included in the CD-ROM).

The book contains an overview of the successful methodologies that have led to new results, sketches and vignettes detailing the development of those methodologies, and a large number of open problems that will intrigue computer scientists, logicians, and mathematicians. The aim of the book is not to give detailed abstract theory relating to automated reasoning. Rather, the goal is to show how these new methodologies are being successfully applied to tackle significant open problems. The result is a volume that is accesible both to the new resercher, and yet contains information that will prove valuable even to the expert.

From a historical perspective, Wos's new book offers the reader an insider's perspective on the research ethic of the automated reasoning group at Argonne National Laboratory. The reader comes away from the book with a deep appreciation of how that ethic, combined with Wos's playful curiosity, has spawned significant gains in the field of automated reasoning.