The second edition of this book is an update and a revision of its first edition (1990; Zbl 0692.68002). The book treats propositional logic, first-order logic and first-order logic with equality. For each of these, resolution and semantic tableau systems are presented as (refutation-based) proof procedures; also, soundness and completeness results of the theorem provers considered are established. Based on Robinson’s unification algorithm, implementations of semantic tableaux in Prolog are given, and similar implementations of resolution procedures are outlined as projects. Additional proof procedures are specified, e.g., axiom systems (Hilbert systems), natural deduction, and Gentzen sequents. For each level of logic considered in this book, the necessary semantical background is considered: Boolean valuations in the propositional case, models in the first-order case, and normal models in the first-order case with equality. Additionally, various fundamental formal properties are derived, e.g., for first-order logic the replacement and skolemization Theorem, Herbrand’s Theorem, Gentzen’s Theorem, the cut elimination Theorem, Craig’s interpolation Theorem, Beth’s definability Theorem, and Lyndon’s homomorphism Theorem. Throughout the book, a system of uniform notation is used (following Smullyan).