5.1 Predicate Logic5.2 Syntax5.3 Semantics5.4 Equivalence and Normal Forms5.5 Herbrand Theories5.6 Semantic Trees 5.7 Resolution 5.8 Strategies for Resolution 5.9 SATCHMO