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 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.