For anyone interested in automated reasoning, this book is not only a great place to start investigating, but a source of inspiration and problems to study for years to come. The authors’ enthusiasm for this area is clearly evident throughout the book. Those who wish to journey down this road will find the book self-contained in that all the necessary prerequisites are included in the first three chapters. The following chapters provide innovative applications and discussions of some of the great triumphs of automated reasoning, centered on the solving of open problems. Later chapters focus on additional research problems for those who wish to pursue this area. The book comes with a CD-ROM containing the current version of the automated reasoning program OTTER as well as many of the example files used in the text.