Homework # 1
due September 13

Reading

Please read Chapters 1-2 in your textbook.

Problems

Please do the following problem from the book:

2.2.7 (transitive closure) full natural language proof required

Pattern Matching

Suppose we have the following definition of natural numbers:

::= z $\vert$ s

And further, the following definition of addition: $\begin{mathpar} \inferrule[PlusZero]{ }{\textsf{z} + n = n} \par \inferrule[PlusSucc]{n_1 + n_2 = n_3}{\textsf{s}\, n_1 + n_2 = \textsf{s}\,n_3} \end{mathpar}$

For each of the following possibilities, give the cases that are possible inverting this relation just once.

$A + B = C$ .
$\textsf{s z} + B = C$ .
$A + \textsf{z} = C$ .
$A + A = C$ .
$A + B = \textsf{z}$ .

Graduate Student Assignment

Find names of three ``proof assistants'' used by computer scientists to mechanize proofs. Explain each in a few sentences. Give a URL of a published proof using each system. (Do not mention SaSYLF.)

Submission

Turn this homework in on paper at the start of lecture.

About this document