Logical Foundations of Computer Science,
Quiz 1 for the course
CS CS 5303, Spring 2012

Name ___________________________________________________

Books and notes allowed.

1. Prove that the sets {∨, ¬} and {→, ¬} are sufficient, i.e., that all other propositional connectives can be described in terms of these connectives.

2. Use natural deduction to prove that p → q |− ¬p ∨ q.

3. Use resolution to prove that ¬p |− p → q.

4. Use program synthesis to solve the Archimedes problem re whether the crown was made of gold or of silver. We know that m1 = ρ1 * V1, that m2 = ρ2 * V2, and that based on the values ρ1 and ρ2, we can tell whether the crown was made of gold or of silver:

Assume that we know m1, m2, V1, and V2. Synthesize a program that, based on this data, checks whether the crown was made of gold or of silver.

5. (For extra credit) Prove that there exists an irrational number x for which the power x5 is rational.