Tutorial week 9, solution notes

1.  logical consequence is monotonic:

(watch out: |= is used in two senses, for structure |= Formula,
and for axioms |= formula)

Suppose T |= Q, and X additional axioms.

Show   T U X |= Q.

By def of logical consequence,  want
   all M.  if M |= T U X then M |= Q.

Suppose    M |= T U X;  then M |= T,
now since T |= Q, we have M |= Q.

2.  CWA here lets as add both "not happy(john)" and "not happy(jane)";
this makes the combined theory inconsistent (impossible that the axioms
can all be true).  Note that CWA for definite clauses avoids
this, the extended theory is always consistent.

3.  Completion:

all x. q(x) <-> x = a.
all y. p(y) <-> some x. y = a & not (q(x))

4.

run the program:
?- \+ p(a).
        1      1 Call: p(a) ? 
        2      2 Call: q(_1152) ? 
        2      2 Exit: q(a) ? 
        1      1 Fail: p(a) ? 
yes

\+ p(a) succeeds,
because p(a) fails (NAF invoked here)
p(a) fails because \+ q(_1152) fails;
\+ q(_1152) fails because q(_1152) succeeds.

not p(a) is not consequence of the completion
(question does not ask to show this, but
take model eg with domain {a,b} and q(a), not q(b),
p(a),p(b), and check against completion axioms.

Since Prolog use of NAF here returns yes to a query that
is not logical consequence of the completion, it is unsound.

5.  To solve query  X => Y, add X to the current program clause
    and solve for Y.

For given example:

  add:  a => b => c
  add   a => b
  add   a

Prolog clause versions:

c :- a, b.
b :- a.
a.

and now query of c succeeds.

(NB  uses equivalence of (a => b => b) and ( a & b => c)  ).

6.  for universal, use new constant:

   natural(c) => natural(s(s(c))).

Add  natural(c) to program.

Now use standard Prolog from this point.