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

Name ___________________________________________________

5 pages of handwritten notes allowed.

1. For the case of interval uncertainty, describe simple algorithms for checking the validity of modal logic formulas [](a ≥ b) and ◊(a ≥ b).

2. Solve the following tolerance problem. We are designing a two-span bridge. The first span a is between 100 and 110 m long, the overall length of the bridge should be between 190 and 210. What are the possible values of the second scan for which we can guarantee the desired bounds on the length? In other words, we know that 100 ≤ a ≤ 110. We need to find all the values b for which [](190 ≤ a+b ≤ 210).

3. Solve the following control problem. We are designing a two-span bridge in which the second span b can be adjusted, if necessary, to take any value from 90 to 100. What are the lengths a of the first span for which we can achieve the total length to be between 190 and 210? In other words, we know that 90 ≤ b ≤ 100. Find all the values a for which ◊(190 ≤ a+b ≤ 210).

4. Assume that the property "good grade" is described by a triangular membership function, for which this property is absolutely true for 80 and absolutely false for 90 and 70. Describe an explicit formula for this function. What is the degree to which 86 is a good grade? If we use min as "and", what is the degree to which both 86 and 88 are good grades?

5. Use the given history to check, step-by-step, that the formula []((¬ k & sUt) → ◊([]k)) is satisfied at moment t = 3. In this formula:

The statement says that if a student studies all the way to the test, then this student will learn the material, and will not forget it. In the history below, -- 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
k -  -  -  -  -  -  -  X  X  X
s -  X  X  X  X  X  X  -  -  -
t -  -  -  -  -  -  X  -  -  X

6. Write a program for computing the sum 12 + 22 + ... + n2 for a given integer n, and use program logic to prove this program's correctness.

7. What does it mean that a logic is non-monotonic? To give an example of non-monotonicity, transform the following knowledge base into a Prolog program. This knowledge base consists of three statements: "Students who study well do well on the tests", "Normally, students study well", and "Lazy students are exceptions (i.e., abnormal)".

8. Translate the following English phrases into first order logic. Try to convey the meaning. If appropriate, use modal logic as well.

9. Briefly describe your project for this class.