CS540 Fall 1999
Homework 5 - First-Order Logic, PROLOG and Planning

Assigned: 4/7/00
Due: 4/21/00

1. Translation from English to First-Order Logic

Give a FOL representation for each of the following English sentences; choose (and briefly define) reasonable constants, predicates and functions (Section 7.3, and other portions of Chapter 7, contain useful examples; see also Nilsson's book pages 248-249; Tony is not a relation) in such a way that you can represent the question "Who is a member of the Alpine Club who is a mountain climber but not a skier?" as a FOL wff.

 
    1. Tony, Mike and John belong to the Alpine Club.
    2. Every member of the Alpine Club is either a skier or a mountain climber or both.
    3. No mountain climber likes rain, and all skiers like snow.
    4. Mike dislikes whatever Tony likes and likes whatever Tony dislikes.
    5. Tony likes rain and snow.

 

2. Convert the following to CNF (Conjunctive Normal Form) and INF (Implicative Normal Form):

 

    1. (EX P(X) v EX Q(X)) => EX (P(X) v Q(X))
    2. UX (P(X) => UY( UZQ(X,Y) => ~ UZ R(Y, X)))
    3. UY (UX P(X) => EX( UZQ(X, Z) v UZ R(X, Y, Z)))
    4. UY (UX (P(X) => Q(X, Y)) => (EYP(Y) ^ EZ Q(Y, Z)))

 

3. Unification

For each of the following pairs of atomic sentences, give the most general unifier, if it exists (apply the algorithm and show the steps). If none exists, explain why. W, X, Y and Z are variable symbols, a , b and c are constant symbols, f and g are function symbols, and P and Q are predicate symbols.

    1. Q(X, X, Z) and Q(a, b, c)
    2. P(Y, Y, Z) and P(a, X, b)
    3. P(X, Y, Z) and Q(a, b, c)
    4. P(X, X) and P(g(Y, a), g(Y, b))
    5. P(a, X) and P(a, f(X))
    6. Q(g(W), W, Y) and Q(Z, f(a), f(b))
    7. P(W, g(Y), W) and P(X, X, g(a))
    8. P(X, Y, X) and P(g(Z), a, Z)

 

4. Linear Resolution

Given the formulae (a) -(f) of the knowledge base (KB) and the query (G) formula (g), does the knowledge base entails the query,

i.e. KB |= G? Explain (give all theorems that allow you to answer this question using a proof system).
      1. N(u, b) ^ N(n, b) ^ N(k, b)
      2. UX (N(X, b) => (T(X) v ND(X)))
      3. ~EX(ND(X) ^ M(X, s))
      4. UX (T(X) => M(X, t))
      5. UX (M(u, X) <=> ~M(n, X))
      6. M(u, s) ^ M(u, t)
      7. EX(N(X, b) ^ ND(X) ^ ~T(X))

 

    1. Use linear resolution (in CNF) with initial set of support (start with one of the clauses that came from the negation of the query) with answer extraction (use Ans literal) and show the search tree; show the most general unifier used at each step.
    2. Use linear resolution (in INF) with initial set of support with answer extraction (use Ans literal).
    3. Can you use SLD-resolution to solve this problem? Explain.

 

5. Prolog / SLD-resolution

  1. The function cons(H, T) denotes the list formed by inserting the element H at the head of the list T. We denote the empty list by nil; the list [2] by cons(2, nil); the list [1, 2] by cons(1, cons(2, nil)); and so on. The formula Last(L, E) is intended to mean that E is the last element of the list L. We have the following definite clauses:

    Last(cons(X, nil), X) <=

    Last(cons(X, Y), Z)) <= Last(Y, Z)

    Use resolution SLD with answer extraction to prove EX Last(cons(2, cons(1, nil)), X).

    (Hint: ask <= Last(cons(2, cons(1, nil)), X), remember to "play" DO generating the resolvents).

  2. Answer part (a) applying the following transformation.

Because the notations becomes so clumsy, the following syntactic sugar is usually adopted (see also page 200 of textbook):

nil becomes [] (empty list)

cons(H, T) becomes [H|T]

There are two syntactic simplifications:

[E1 | [E2]] becomes [E1, E2]

examples: [a|[d, nil]] becomes [a, d | nil]

[a, b, c|[d, e, f]] becomes [a, b, c, d, e, f]

[a, b, c|[d, e|F]] becomes [a, b, c, d, e | F]

[E1 | nil] becomes [E1]

examples: [a, b, c | nil] becomes [a, b, c]

using both rules [a|[d|nil]] becomes [a,d]

 

b)Can we prove EX Append([1, 2], [3, 4], X) from the clauses below using Prolog ?

(Hint: ask <= Append([1, 2], [3, 4], X), remember to "play" DO generating the resolvents). Show the steps (by that I also mean the mgu in each step).

Append([ ], X, X) <=

Append([X|L], Y, [X| Z]) <= Append(L, Y, Z)

 

6. Prolog / SLDNF-resolution

Can we prove EX EYdaughter(X, Y) from the clauses below using Prolog?

(Hint: ask <= daughter(X, Y) , remember to "play" DO generating the resolvents). The operator not is negation by failure. Show the steps.

daughter(X, Y) <= female(X), father(Y, X)

daughter(X, Y) <= mother(Y, X), not male(X)

mother(john, mary) <=

 

7. Using Quintus Prolog

  1. Run problems 5 and 6 using Quintus Prolog and check your answers!

    See http://www.cs.wisc.edu/~jgast/cs540/prolog.html for a recipe how to use it.

  2. b) Run this DT learning program in Prolog using this file as data; from the answer (given as a rule) draw the decision tree.

Load both files (program and data), then load the math-library with this command:

load_files(library(math)).

Then run the query:

dtlearn(reads, [e1,e2,e3,e4,e5,e6,e7,e8,e9,e10,e11,e12,e13,e14,e15,e16,e17,e18], [known,new,short,home], DT).

You can use the trace facilities in order to see the computation steps.

8. Problem 11.7 in the textbook - parts a (use "successor-state axiom") and b only (see pages 360 - 362).

  1. using the situation calculus (see pages 204-208, 341-342) with a "successor-state axiom" that combines in a single axiom the effect for this action and the frame axiom;
  2. using STRIPS language (see pages 343-345).