Logical Foundations of Computer Science,
Homeworks for the course
CS 5303/6303, Spring 2016

1. (Due January 27) Form a truth table for implication. Apply the general algorithm for producing a DNF for a given propositional expression to generate a Disjunctive Normal Form for implication.

2. (Due January 27) Prove that the set consisting of a single propositional operation NOR is sufficient, i.e., that all other propositional connectives can be described in terms of NOR.

3. (Due January 27) Prove that the OR operation is monotonically increasing in both of its variables. Explain how this can be used to prove that the set consisting of a single OR operation is not sufficient, i.e., that not all propositional connectives can be described in terms of OR. Prove that implication is not monotonically increasing in each of its variables.

4. (Due January 27) Prepare a preliminary proposal for a class project.

5. (Due February 1; submit by January 27 for extra credit) Prove that XOR and AND satisfy distributivity property, similar to addition and multiplication. Explain how this can be used to prove that the set consisting of a single XOR operation is not sufficient, i.e., that not all propositional connectives can be described in terms of XOR.

6. (Due February 1; submit by January 27 for extra credit) Use truth tables to prove that p & q |= p → q.

7. (Due February 1; submit by January 27 for extra credit) Use natural deduction to prove that p & q |− p → q.

8. (Due February 1) Apply the general algorithm for producing a CNF for a given propositional expression to generate a Conjunctive Normal Form for implication.

9. (Due February 1) Use resolution to prove that p & q |− p → q.

10. (Due February 3) Use program synthesis to solve the following problem about the generic triangles, with three sides a, b, c, and three angles A, B, and C. The relations are:

We know a, b, and A, we need to find all other variables.

11. (Due February 3) Do exercises at the end of Chapter 4 of the online book, Parts A-D (except the ones that we did in class).

12. (Due February 8) Do remaining exercises at the end of Chapter 4 of the online book (except the ones that we did in class).

13. (Due February 10) Use the general algorithm to translate the following first order formulas into the normal form:

14. (Due February 15; submit by February 10 for extra credit) For each of the syllogisms described in Part B of exercises at the end of Chapter 4, perform two derivations: by using resolution and by using natural deduction. (Of course, you do not have to do those syllogisms that we did in class.)

15. (Due February 15; submit by February 10 for extra credit) For all problems from Part D of exercises at the end of Chapter 4, check whether the derivation is correct: either produce a formal derivation (by using either resolution or natural deduction) or show a counterexample.

16. (Due February 15) Translate into logic:

17. (Due February 22) For each of the syllogisms described in Part B, use step-by-step Prolog derivation to check which of the syllogisms are true.

18. (Due February 22) Use predicates parent(Parent, Person), male(Person), and female(Person) to describe the Prolog rules that describe aunt, uncle, and grandfather. Add facts about your own relatives (or if you prefer, about fictitious relatives), and show how Prolog will derive who is whose aunt and uncle.

19. (Due March 16) Use the Prolog website to derive a simple fact about your own relative.

20. (Due March 16) For the case of interval uncertainty, come up with simple algorithms for checking the validity of modal logic formulas [](a ≤ b) and ◊(a ≤ b).

21. (Due March 21) Solve the following tolerance problem: Let us assume that 10 ≤ a ≤ 12. Find all the values b for which [](17 ≤ a+b ≤ 22).

22. (Due March 21) Solve the following control problem: Let us assume that −4 ≤ b ≤ 6. Find all the values a for which ◊(−2 ≤ a+b ≤ 4).

23. (Due March 28) Write a program that implements a multi-valued logic approach to expert-based control that we covered in class (and which is described in the handouts). This program should take, as input:

and return the angle φ to which we need to turn the knob of the temperature controlling device to compensate for this difference. Submit a printout of the program, a printout of the results, and be ready to show how your program works.

24. (Due March 30) Use the given history to check, step-by-step, that the formula []((p & ¬o) → (X(s & (s U o)) & [](o → []o))) is satisfied at moment t = 2. In this formula:

In the history, -- means that a property was not satisfied at a given moment of time, while X means that the corresponding property was satisfied. The history is as follows:
    1  2  3  4  5  6  7  8  9 10
  p X  -  X  -  -  -  -  X  -  -
  s -  -  -  X  X  X  -  -  -  -
  o X  -  -  -  -  -  X  X  X  X

25. (Due April 4) Give an example showing that Prolog describes non-monotonic logic.

25a. (Due April 6) Write a program that, given two computable numbers x and y, returns their sum and their difference.

26. (Due April 11) Write a program that, given two computable numbers x and y, returns their product.

27. (Due April 13) Solve problems 1-5, 7, and 8 from 2012 Test 2.