5.1 Predicate Logic5.2 Syntax5.3 Semantics5.4 Equivalence and Normal Forms5.5 Herbrand Theories5.6 Semantic Trees5.7 Resolution5.8 Strategies for Resolution5.9 SATCHMO