This book shows how computers can be programmed to reason. It introduces the field of automated reasoning through examples and puzzles. The automation of reasoning has advanced markedly in the past few decades, and this book therefore discusses some of the remarkable successes which 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 also answers), as well as tutorial chapters that gently introduce...

Automated reasoning programs are successfully tackling challenging problems in mathematics and logic, program verification, and circuit design. This two-volume book includes all the published papers of Dr Larry Wos, one of the world's pioneers in automated reasoning. It provides a wealth of information for students, teachers, researchers, and even historians of computer science about this rapidly growing field.

The book has the following special features:

(1) It presents the strategies introduced by Wos which have made automated reasoning a practical tool for solving challenging puzzles...