13.2
(implies {and (going_to x y) (weather raining y)} [get x umbrella] )
(implies {and (going_to x y) (weather raining y)} [get x raincoat] )
(implies {and (going_to x y) (weather snowing y)} [get x boots] )

13.4
if 1>0 then fac(1) = 1*fac(0); 1>0 thus fac(1)=1*fac(0)
fac(0)=1 is true, thus fac(1)=1*1=1;
if 2>0 then fac(2) = 2*fac(1); 2>0 thus fac(2)=2*fac(1)
fac(1)=1 thus fac(2)=2*1=2;
if 3>0 then fac(3) = 3*fac(2); 3>0 thus fac(3)=3*fac(2)
fac(2)=2 thus fac(3)=3*2=6;

14.2
A=>B converts to (-A v B)
(B ^ C) => D                 converts to (-(B ^ C) v D) converts to (-B v -C v
D)
(D ^ (E v F)) => G         converts to (-(D ^ (E v F)) v G)
                        converts to (-D v -(E v F) v G)
                        converts to (-D v (-E ^ -F) v G)
                        converts to (-D v -E v G) ^ (-D v -F v G)


14.3
a. {((p=>q) ^ -p) => -q} converts to ([-p v q] ^ -p) => -q
converts to {-([-p v q] ^ -p) v -q}
        converts to {-[-p v q] v p v -q}
        converts to {[p ^ -q] v p v -q}
        converts to {p v -q) ^ (p v -q) converts to (p v -q)

b. EuEvAwAxEyAzEqAs p(q, s, u, v, w, x, y, z)
        EvAwAxEyAzEqAs p(q, s, U, v, w, x, y, z) U a constant
        AwAxEyAzEqAs p(q, s, U, V, w, x, y, z) V a constant
        AwAxAzEqAs p(q, s, U, V, w, x, Y(w, z), z) Y a function
        AwAxAzAs p(Q(w, x,z), s, U, V, w, x, Y(w, z), z) Q a function

c. Ax|{P(a,x) => Ey|Q(a, y, x)}
        Ax|{-P(a,x) v Ey|Q(a, y, x)}
        Ax Ey{-P(a,x) v Q(a, y, x)}
        Ax {-P(a,x) v Q(a, Y(x), x)}        Y a function

d. Ax|{P(a,x) => Ex|Q(a, y, x)}
        AxEz|{-P(a,x) v Q(a, y, z)}
        Ax|{-P(a,x) v Q(a, y, Z(x))} Z a function

e. Ey|((Ax|(P(x) => Q(f(x), y))) => ((Ey|P(y)) => (Ex|Q(x, y))))
        Ey|( -(Ax|[-P(x) v Q(f(x), y)]) v ( -(Ey|P(y)) v (Ex|Q(x, y))))
Ey|( (Ex|[-P(x) v Q(f(x), y)]) v ( (Ay|-P(y)) v (Ex|Q(x, y))))
Ex|[-P(x) v Q(f(x), Y)] v AyEx|(-P(y)  v Q(x, Y))
Ex AyEz |[-P(x) v Q(f(x), Y) v -P(y)  v Q(z, Y)]
AyEz |[-P(X) v Q(f(X), Y) v -P(y)  v Q(z, Y)]
Ay |[-P(X) v Q(f(X), Y) v -P(y)  v Q(Z(y), Y)]


14.4
I assume I have eval_cnf(e, alist) like one from a prior chapter that
evaluates such logic expression e using assignments in alist. Then I will
show unsatisfiability by generating all possible interpretations, i.e. all
possible substitutions of t or f for each variable. If any of these
interpretations evaluate to t, stop because its not unsatisfiable.

Unsat(e, let) = unsat2(e, let, nil) where

Unsat2(e, let, alist) = //return t if all interpretations return false
        If null(let)
        Then not(eval_clause(e, alist))
 // when there's no more vars in let, then alist has a full interpretation
// and then if interpretation is true, then return false
        Elseif unsat(e, cdr(let), (car(e).t).alist) // add the true case
for the next variable
        Then unsat(e, cdr(let), (car(e).f).alist)  // add the false case
for the next variable
        Else false

You didn't really need to show eval_cnf but it might look something like:

Eval_cnf(e, alist)  = // returns e evaluated under substitution alist
        If null(e)
        Then true
        Elseif eval_clause(car(e), alist)
        Then eval_cnf(cdr(e), alist)
        Else false

Eval_clause(e, alist) = // evaluate the list of literals in the clause e
        If null(e)
        Then true  // empty clauses are true
        Elseif eval_literal(car(e), alist)  // if first literal is true,
quit with true
        Then true
        Else eval_clause(cdr(e), alist)  // otherwise try next literals

Eval_literal(e, alist) =
        If not(atom(e))  // if literal is not an atom (i.e. a list)
        Then not(eval_literal(cadr(e), alist))  // then this must be a NOT
        Else let z=assoc(e, alist) in  // look up literal in alist
                If  null(z) then "error" else cadr(z) and it should be
there, so return value