Introduction to Artificial Inteligence - Spring 2001

Inference in FOL

1. Inference rules involving quantifiers
   • Universal elimination
   • Existential elimination
   • Existential introduction
2. Example proof
3. Generalized modus ponens
   • Canonical form (Horn, conjunctive)
   • Unification
   • Simplified proof using generalized modus ponens
4. Forward chaining
5. Backward chaining
6. Completeness
7. Generalized resolution and theorem proving
   • Resolution inference rule
   • Canonical forms for resolution: conjunctive, implicative
   • Resolution proofs
   • Conversion to normal form
   • Example proof
8. Resolution strategies
   • Unit preference
   • Set of support
   • Input resolution
   • Linear resolution
   • Subsumption