Section 3 : Inference in first-order logic

Commentary

Section Goals

• To discuss the basic ideas behind first-order inference; i.e., unification and reduction to propositional inference.
• To introduce main techniques regarding inference in first-order logic, such as resolution, theorem-proving, and forward and backward chaining.
• To introduce basic knowledge about logic programming.
• To introduce relevant algorithms of the above inference methods.

Section Notes

• Parts of this section may be skipped by those who have a strong background in first-order logic. However, even for those students, further study of the in-depth issues in this section is encouraged to pave the way for the future sections and units

Learning Objectives

Learning Objective 1

• Exemplify logical agents in the context of the wumpus world.
• Outline the syntax and semantics of propositional logic.
• Outline the basic principle of propositional entailment.
• Describe how logic programming is used to represent and solve inference problems.
  • Explain the following concepts or terms:
  • Universal and existential instantiation
  • Skolemization
  • Propositionalization
  • Substitution
  • Unification
  • Predicate indexing
  • Subsumption lattice
  • Datalog
  • Conjunct ordering
  • Forward chaining
  • Incremental forward chaining
  • Rete algorithm
  • Production system
  • Magic set
  • Backward chaining

Objective Readings

Required readings:

Reading topics:

Inference in First-Order Logic (see Chapter 9 of AIMA3ed).

Supplemental Readings

Bratko, I. (2001). Prolog programming for artificial intelligence (3rd ed.). Toronto, ON: Addison-Wesley.

Objective Questions

• What techniques can be used in improve forward and backward chaining, respectively?
• What are the steps to convert first-order logic sentences into conjunctive normal form (CNF)?
• What is the difference in representing and solving inference problems between logic programming and resolution (or theorem proving)?
• Is first-order logic resolution complete?
• Explain how to deal with equality in resolution.

Objective Activities

• Explore the strengths and applications of logic programming languages and tools, such as SWI-Prolog (https://www.swi-prolog.org/).
• Explore the following first-order inference algorithms from the textbook's website.
  • Substitution
  • Unify
  • FOL-FC-Ask
  • FOL-BC-Ask
  • Otter
• Complete Exercise 9.3 of AIMA3ed.
• Complete Exercise 9.6 of AIMA3ed.
• Complete Exercise 9.7 of AIMA3ed.
• Explore other relevant fields, such as deductive database and constraint logic programming (CLP).