The propositional logic is presented as a simple language with its syntax and semantics. The semantic notions of models, satisfiability, validity, etc., are carried over to all logics in later chapters. This chapter presents various normal forms of propositional formulas, including the binary decision diagram (BDD) as a special normal form. After a brief introduction of three types of optimization problems, the chapter shows how propositional logic is used in programming languages and problem solving.