Class 32: Logic Programming (2)

Held: Wednesday, April 19, 2006

Summary: Today we consider the basics of the Prolog logic programming language.

Related Pages:

• EBoard.
• Comments on Prolog reading.

Notes:

• Questions on the exam?
• I suppose a detailed analysis of "The Story of Mel" would make an interesting presentation.
• Reading for Friday: The Birth of Prolog.

Overview:

• Prolog: Imposing Fixed Control on Horn-Clause Logic.
• Some Examples.
• The Need for Backtracking.
• Problems with Resolution.
• Affecting Control: Cut.

Prolog: Imposing Fixed Control on Logic

• Prolog is the standard programming language based on predicate logic.
• Prolog, in general, uses Horn clause form.
• Prolog imposes a fixed control on the logic of the program.
• The evaluation strategy is fairly simple.
  • At any point, Prolog has a sequence of goals to solve.
  • It picks the first unsolved goal.
  • It picks the first clause whose consquent "matches" the goal (that is, we can choose an assignment of values to variables so that the goal and the consequent are identical).
  • It replaces the goal with precedents of the clause (substituting as necessary).
  • If it eventually runs out of goals, it notes that the goals have been solved, and reports substitutions.
  • If it cannot find a matching clause, it "backs up" an earlier decision and tries a different clause.

Some Examples

Reasoning about courses

• Suppose I'm trying to figure out what courses someone has, given partial knowledge.
• Knowledge is represented in two ways:
  • took(Person,Course) indicates that Person took a particular course.
  • prereq(PreReq,Course) indicates that PreReq is a PreReq for Course.
• I might know, for example, that Davis has taken CSC302, CSC362, and CSC151.
• Might also know that CSC301 is a prereq for CSC302, that CSC152 is a prereq for CSC301, that MAT218 is a prereq for CSC301, and so on and so forth.
• How should we relate took and prereq?
• I might ask whether Davis has taken CSC301.

Simple Numeric Reasoning

• Let's represent numbers as lists of ones.

  add([],X,X).
  add([1|X],Y,[1|Z]) :- add(X,Y,Z).
  

The need for backtracking

• If I ask whether Davis has taken CSC152, and choose the wrong way to prove it, I may end up with a dead end.
• I must therefore back up and try another proof strategy.

Problems with Resolution

• See the paper for the resolution algorithm.
• It does, however, have problems.
• Consider how we might resolve
  { foo(f(X0),X0); foo(X1,f(X1)) }
• The first mistmatch is f(X0) vs X1.
• We therefore substitute f(X0) for X1
{ foo(f(X0),X0); foo(f(X0),f(f(X0)) }
• The next mismatch is X0 vs. f(f(X0))
{ foo(f(f(f(X0)),f(f(X0))); foo(f(f(f(X0))),f(f(f(f(X0)))) }
• Whoops, we have the same mismatch. Infinite recursion may result.

Affecting control: Cut