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

Name ___________________________________________________

5 pages of handwritten 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 ∨ q |− ¬p → q.

4. Use truth tables to prove that p ∨ q |= ¬p → q.

5. Use program synthesis to solve the following problem from high school physics. Suppose that at moment 0, a toy rocket located at a point 0 is launched. At moment t, it reaches distance d = vx * t from the launch pad, where vx is the horizontal velocity. The rocket's height at time t is equal to h = vz * t - (1/2) * g * t2, where vz is the initial vertical velocity, and g is the acceleration of the free fall (= 9.81 m/sec2). Suppose that we know vx, vz, and d, and we need to predict the height. Use Horn clauses to synthesize the corresponding program. Hint: if you do not remember how to solve the quadratic equations, do not worry, in this problem, there is no need to solve it.

6. Prove that there exists an irrational number x for which the power x7 is rational.

7. Use resolution to prove that if we have ∀x∀y∀z (x ~ y & y ~ z → z ~ x) and ∀x (x ~ x), then ∀x∀y (x ~ y → y ~ x).

8. Use the predicates S(x) (x is a student), E(x, y) (x eats y), and L(x, y) (x likes y) to translate the following statements into predicate logic:

9. Suppose that we have Prolog predicates parent(P, C), male(X), and spouse(X, Y). Write down Prolog rules that describe father-in-law(FL, X) and mother-in-law(ML, X) in these terms. Give an example of using these rules.