CS486 Applied Logic Final Assignment Due Thurs, May 3, 2001

Reading: Please read Stewart & Tall, p. 172-182, Chapter 13.

Exercises:

1. Write a careful proof of the stamps theorem from lecture, showing explicit use of these rules: induction on integers, recursive definition (reduce),
ÚL, ÚR, "L, "R, arith, and equality.

The equality rules include those for hd, tl and cons such as

hd(a.t)=a, tl(a.t)=t and l¹[ ]Þ(hd(l).tl(l)=l).

2. Write a program to compute the function specified by stamps.

3. Sketch a proof of this conjecture:

Define x is_on l = if x=[] then 0;

else if x=hd(l) then 1;

else x is_on tl(l).

Show "l:list. "i:int. (1£i£length(l)Þ(index(i,l) is_on l)=1

4. Discuss the issue of how logic can help in specifying programming tasks and how careful proof helps prevent errors in program design.

`