Class 23: Logic Programming, Continued

Held Wednesday, March 17

Summary

Contents

Notes

• Are there any questions on the exam?
  • I'll try to be around for much of tomorrow so that I can answer questions on the exam.
  • Because of problems with the MathLAN, the exam is now due after break.

Predicate-Logic Programming

• How might we use the predicate logic as a programming language? We could state "theorems" and ask the system to prove the theorems based on the rules of predicate logic and the definitions contained within our program. In effect, we state our theorem as a question and ask the program to answer it.
  • For example: "Is Socrates mortal?" "Yes, because Socrates is a person and all people are mortal."
  • Similarly: "Are there any mortals?" "Yes, Socrates is a mortal because Socrates is a person and all people are mortal."
  • Similarly: "Is Socrates immortal?" "No, because Socrates is mortal (see above) and no mortal is immortal."
  • And "Is Lou Reed influential?" "Yes, because Lou Reed was a member of the Velvet Underground and R.E.M. were influenced by the Velvet Underground."
• How might we implement such a language? Well, there are two aspects, depending on the type of question that is being asked.
  • To prove a theorem about an atom. In this case, we might "plug" the atom in to the right hand side and then attempt to prove the right hand side.
  • To prove a theorem about a variable, we may need to "guess" instantiations and plug in.
  • Note that the first quickly becomes the second. For example, in proving that Lou Reed is influential, we need to identify a band that Lou Reed was/is a member of. Then, we need to determine whether that band is influential.
• It turns out that some aspects of such proofs are extremely difficult. In particular, it may be impossible to prove a negation.
• To simplify matters, we may want to write a disjunction of Horn clauses: clauses that define predicates in which consist of only an and of assertions (i.e., no nots, the only ors are used around our horn clauses).
• In such a system, we have a simpler nondeterministic proof strategy: pick a rule that defines a predicate and attempt to prove each component of the right hand side.
• Of course, that leads to the question of how to deal with the nondeterminism. We'll return to that question later.

History

• Created Tuesday, January 19, 1999 as a blank outline.
• Filled in some details on Monday, March 15, 1999. Many were taken from the previous outline, and were there taken from outline 32 and outline 33 of CS302 98S.
• Removed some uncovered material on Friday, March 19, 1999.