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

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. Hint: use an axiom a ∨ ¬ a for an appropriate a.

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

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

5-6. Use program synthesis to solve the following problem. For an electric circuit, the voltage V, resistance R, current I, and power P are related by the following formulas: V = I * R (Ohm's Law) and P = V * I. Suppose that we know the voltage V = 110 V and the power P, and we need to estimate the resistance R. Use the wave algorithm to synthesize the program. Then show how a similar program can be synthesized by using Prolog.

7-8. Use resolution to prove that if we have ∀x (Ax → Bx) and ∃x (Ax ∧ Cx), then ∃x (Bx ∧ Cx). Prove the same statement by using natural deduction.

9. Use the predicates C(x) (x is a cat), L(x, y) (x likes y), and P(x, y) (x likes to plays with y) to translate the following statements into predicate logic:
  • Cats like to play with other cats.
  • Some cats do not like to play.
  • Some cats only play with those they like.

10. Suppose that we have Prolog predicates parent(P, C), male(X), and female(X). Write down Prolog rules that describe grandfather(GF, X) and grandson(GS, X) in these terms. Give an example of using these rules.