This chapter discusses various types and styles of proof techniques for the propositional logic and introduces the semantic tableau method and three special inference systems: Hilbert system, natural deduction, and resolution. It then presents the algorithm of Boolean constraint propagation (BCP), which is a decision procedure for propositional Horn clauses. An implementation of BCP in linear time is described, using the head/tail literal technique.