This book is dedicated to a comprehensive presentation of the classical decision problem of first-order logic. The centrality of the original decision problem (which can be stated equivalently as the satisfiability problem for formulas, the validity problem for sentences, or the provability of formulas in a sound and complete formal system) has been identified by the founders of mathematical logic. Subsequent developments in mathematical logic and theoretical computer science, especially the formalization of the notion of computable function by Gödel, Kleene, and Herbrand, yielded a negative answer to the classical decision problem and focused the attention of researchers towards the identification of fragments of first-order logic that are decidable or undecidable.