CS 201

Mathematical Foundations of Computer Science

Sample Test #1

Note: the real test will be a sheet of paper, typeset, so that logical expressions will be easily readable!

This test is in-class, open-book, open-notes; total time is 50 minutes. There are 4 questions, each worth the same number of points.

Negate the following two logical expressions: forall x exists y [(exists z [z xor y]) -> (x and (not y))] exists x [(forall y (x ->y)) or (exists z (x and z))]
Prove by contradiction: ((n is prime) and (n <> 2)) -> (n is odd)
Prove by induction: sum from (i=1) to (i=n-1) (2i-1)² = n(4n²-1)/3
Consider the following small piece of code
```
z <- x
w <- y
while w > 0 do
  z--
  w--
return z
```
Verify that it computes z=x-y by asserting and proving a suitable loop invariant.
(This is a while loop, but the index for the loop still exists: in this case it is w.)

Be as formal as possible in your write-up. For each theorem to prove, state the hypothesis, the conclusion, which proof method you are using. When using induction, state what needs to be proved in the basis; state what is the inductive hypothesis and what needs to be proved in the step.