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.