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.

`