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

1. (Due January 23) Exercise 1.1 from the book.

2. (Due January 25) Prove that the square root of 3 is irrational.

3. (Due January 25) Prove that there exists an irrational number x for which x raised to the square root of 3 power is rational.

4. (Due January 30) Exercise 1.2, Part 3, (a)-(e); Exercise 1.5, Part 2, Part 3(a), and Part 5.

5. (Due February 8) Use the Horn clauses and wave algorithm to solve the following problem: we know that V = V1 + V2, V1 = I * R1, V2 = I * r2, V = I * R, we know the values of I, R1, and R2, we need to find R.

6. (Due February 8) Exercise 2.1, Part 1)-4).

7. (Due February 20) Use resolution to prove the following two statements: (a → b) → (¬b → ¬a) and (a & b → c) → (a & ¬b → ¬c).

8. (Due February 20) Use resolution to prove that if we have ∀x∀y∀z (x > y & y > z → x > z) and ∀x (¬x > x), then ∀x∀y (x > y → ¬y > ¬ x).

9. (Due February 27) Use the Prolog website to derive a simple fact about your own relative.

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

11. (Due March 21) Solve the following tolerance problem: Let us assume that 9 ≤ a ≤ 11. Find all the values b for which [](18 ≤ a+b ≤ 21).

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

13. (Due March 28) select a project.

14. (Due April 2) 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, the difference ΔT between the actual temperature T and the ideal temperature T0, 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.

15. (Due April 9) Finish what we started in class: use the given history to check, step-by-step, that the formula []((p & ¬o) → X(s & (s U o)) & [](o → []0) 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  -  -
s -  -  -  X  X  X  -  -  -  -
o -  -  -  -  -  -  X  X  X  X

16. (Due April 9) Use the given history to check, step-by-step, that the formula [](t → X◊p) & [](p → ¬Xp) is satisfied at moment t = 2. In this formula:

The history is as follows:
  1  2  3  4  5  6  7  8
t -  -  X  -  -  X  -  -
p -  -  -  -  X  -  X  -

17. (Due April 11) Similarly to what we did in class, write a program for computing an, and use program logic to prove this program's correctness.

18. (Due April 16) Come up with two ambiguous English phrases, and propose a reasonable translation of each of these phrases from English to predicate logic.