The aim of this book is to serve both as an introduction to automated theorem proving (ATP) in first-order logic, and as a guide to current work on particular aspects of ATP. The intention is to give full details of the princi......