Summary

In this section we have introduced first-order predicate logic, and explained proof by resolution as a method of sound logical inference. We outlined unification and briefly mentioned Horn clauses and the existence of Prolog.

Logic might seem the answer to everything, but there are some difficulties.

• How in the proof were we clever enough to pick up the right clauses. Certainly by matching P, P pairs, but also by using our intuition to find a solution. If we have to use intuition, the machine has to search.
• There are limits to pure logic, but if we introduce extras, our simple-minded rules won't always work.
• Machines are going to need search strategies for looking into the database. In turn these searches might suffer from:

  • Combinatorial explosion
  • The halting problem - search is not guaranteed to terminate

   

<<<Previous Next Section >>>