The good news is that, even though evaluation and satisfaction are not directly computable, there are effective procedures for indirectly determining validity, contingency, unsatisfiability, logical entailment, and so forth that work in many cases even when our usual direct methods fail. The key is symbolic manipulation of various sorts, e.g. the generation of proofs, which we describe in the next few chapters. But, first, in order to gain some intuitions about the power of Herbrand Logic, we look at some examples.
