In the 1930s Kurt Gödel, Alonso Church, and Alan Turing laid important foundations for logic and theoretical computer science. Of particular interest for AI are Gödel’s theorems. The completeness theorem states that first-order predicate logic is complete. This means that every true statement that can be formulated in predicate logic is provable using the rules of a formal calculus. Using programmable computers, on this basis, automatic theorem provers could later be constructed as implementations of formal calculi. We introduce the language of first-order predicate logic, develop the resolution calculus, and show how automated theorem provers can be built and applied to prove relevant problems in every day reasoning and software engineering.