I will describe some of the highlights of the history of how automated theorem proving developed, and some of the main areas of interest. I will then precisely define some foundational material and talk about decision methods for propositional logic (SAT).