Outline Reducing first-order inference to propositional inference ·Unification Generalized Modus Ponens ·Forward chaining ·Backward chaining ·ResolutionOutline • Reducing first-order inference to propositional inference • Unification • Generalized Modus Ponens • Forward chaining • Backward chaining • Resolution