In the earlier chapters of Part III we introduced the propositional and predicate calculi and described how well formed expressions were formed. In ► Chap. 9 we present rules for reasoning with these expressions. There are three major sections to ► Chap. 9 . The first introduces the resolution refutation technique for reasoning with facts and rules expressed in the propositional or the predicate calculus. ► Section 9.2 demonstrates how resolution is used, first changing facts and rules into Horn clause form, then introducing search procedures that, using unification and resolution algorithms, can produce conclusions. In an important practical application, resolution theorem proving using the resolution refutation system, has made the current generation of Prolog interpreters possible; see ► Sect. 9.3.