• 9.1 introduce inference rules for quantifiers and shows how to reduce first-order inference to propositional inferene
• 9.2 describes how unification can be used to construct inference rules that work directly with first-order sentences
• discuss 3 major families of first-order inference algorithms
  • 9.3: forward chaining
  • 9.4: backward chaining
  • 9.5: resolution-based theorem proving

1. Propositional vs. First-Order Inference

One way to do first-roder inference is to convert the first-order knowledge base to propositional logic and use propositional inference.

• Univerial Instantiation
• Substitution
• Existential Instantiation