1.
(a) Constants: polly, sam, bert, pete
  There are no function symbols
  Predicates: flies, bird, bee, parrot, skua, bumbleBee, penguin
(b):The ground terms are: polly, sam, bert, pete
(c) there are 28 ground atomic formulas, each has the form p(c) where p is
  one of the 7 predicate symbols and c os one of the 4 constants
(d) f(Y) = {parrot(polly),skua(sam),bumbleBee(bert),penguin(pete)} \union
        {flies(c) | (bird(c) \in Y) \or (bee(c) \in Y), c constant} \union
        {bird(c) | (parrot(c) \in Y) \or (skua(c( \in Y), c constant} \union
        {bee(c) | bumbleBee(c) \in Y, c constant} \union Y
(e) f({}) = {parrot(polly),skua(sam),bumbleBee(bert),penguin(pete)}
    f^2({}) = f({}) \cup {bird(polly),bird{sam),bee(burt)}
    f^3({}) = f^2({}) \cup {flies(polly),flies{sam),flies(burt)}
    f^4({}) = f^3({}) = least fixed point
(f) Herbrand universe = {polly, sam, bert, pete}
  constants are interpreted as themselves, e.g., polly^H = polly, etc.
  for each predicate p, define p^H to be function mapping c to true if
  p(c) is in the least fixed point of f, so:
    parrot^H(c) = true  <=>  c = polly
    skua^H(c) = true  <=>  c = sam
    bumbleBee^H(c) = true  <=>  c = bert
    penguin^H(c) = true  <=>  c = pete
    bird^H(c) = true  <=>  c in {polly,sam}
    bee^H(c) = true  <=>  c = bert
    flies^H(c) = true  <=>  c in {polly,sam,burt}

2.
(a) CWA(T) = T \union {\not rich(karen), \not poor(keith), \not happy(keith)}
(b) Consider T' = T \union {happy(keith)}
  Then T \subseteq T', and CWA(T) |= \not happy(keith)
  but it is not the case that CWA(T') |= \not happy(keith)
(c) Yes, for this example CWA(T) does predict the behaviour of Prolog
  negation by failure since Prlog answers yes to \+ A, wher A is a ground
  atomic formula, only for exactly the 3 cases 

     A = rich(karen), poor(keith), happy(keith)

  that CWA(T) negates.
(d) The Clark completion is:
      \forall X.  happy(X) <-> poor(X)
      \forall X.  poor(X)  <-> X = karen
      \forall X.  rich(X)  <-> X = keith
      \neg (karen = keith)
(e) Yes, Clark completion does exhibit non-monotonicity.
    Consider T' as in (b), then Comp(T') is:
      \forall X.  happy(X) <-> (poor(X) or X = keith)
      \forall X.  poor(X)  <-> X = karen
      \forall X.  rich(X)  <-> X = keith
      \neg (karen = keith)
  So  T \subseteq T', and Comp(T) |= \not happy(keith)
  but it is not the case that Comp(T') |= \not happy(keith).

3. CWA gives:
       happy(tweedledum) \or happy(tweedledee)
       \not happy(tweedledum)
       \not happy(tweedledee)
 The problem is this is inconsistent!

4. When there are no function symbols, the set of ground atomic formulas
 (for the signature of predicates and constants appearing in program and 
 query) is finite. One can then explcitly construct the minimum Herbrand
 model by computing the least fixed-point of the function corresponding to
 the program, as in Question 1. The validity of the query is then decided
 mrely by checking if there is a tuple of constants, instantiating the 
 existential quantifiers, for which the resulting conjunction of ground atomic
 formulas are all true in the minimum herbrand model (i.e., contained in the
 least fixed-point set).
 [Double-check that students understand why the set of ground atomic formulas
  becomes infinite once a single unary function symbol is present.
  Also, clarify that decidability for the function-symbol-free frangment is
  specifically a property of definite clause logic. General predicate logic for
  a single binary predeicate (no function symbols, no constants) is 
  undecidable.]