Meeting 13: Unification in FOL

Reading: AIAMA 9.1-9.2

Now that we can define FOL knowledge-bases we need to be able to do inference. An important step in this process is the ability to parse and match two FOL expressions using the unification algorithm.

Questions you should be able to answer after reading are:

  1. What is universal instantiation?
  2. What is existential instantiation?
  3. What is skolemization?
  4. How does one reduce a FOL KB to a PL one?
  5. Why is inference in FOL semi-decidable?
  6. What is the lifted version of modus ponens?
  7. What is unification?
  8. What is the most general unifier for a given sentence pair?

Focus on the unification algorithm in Fig 9.1 You should also be able to trace its execution for example inputs.