[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/11
[Index] || [Contents] || [Grades] Mon Mar 3 14:43:02 PST 2003
656/556 2003 1w 11 Midterm
Assigned work: Prepare a 2sided "cheat sheet" 11><8.5 for
	the midterm.  Hand in with midterm for 3pts.

Formal Methods MidTerm -- Logic -- 60 points Max
You may use a calculator, but no computers or wireless devices.  Put answers
 on the exam paper. There are ?? questions. Each is worth 10 points maximum.
  Attempt 6 questions ONLY.  More than 6 answers will not count. Do your best
 questions first. List the numbers of the questions you want graded below.  
 I will ignore questions that are not listed below:
Qn #	___	___	___	 ___	 ___	___
In questions 1,2,3,7,8, and 9 use the text's notations for propositions and predicates.
In questions 4,5, and 6 use the texts notation for Boolean Algebra.

1. Draw parse tree of the following well-formed formula of the 
	Propositional Calculus. ... Derive/Prove the above well-formed 
	formula by using the natural deduction system presented in the book.

2. Use a table to verify that the formula ...  is valid.

3. Translate to well-formed formulae of the Propositional Calculus

4. Convert OBDDs to Boolean Expressions

5. Draw OBDDs of given Boolean Expressions

6. Combining/Merging two OBDDs to give one
    using the "apply" and "reduce" algorithms

7. Draw parse tree of the following well-formed formula 
   of the Predicate Calculus.  What is the scope of the variable ...
   in this formula?(2 pts)

8. Prove the following theorem of the Predicate Calculus
    either by using natural deduction or a semantic tableaux.

9. Translate ... into well-formed formulae of the Predicate Calculus
	 and spot ambiguities.


Assigned work: Study chapter 3 sections 3.1 and 3.2
	And handouts.


next: Given a complex program in a complex environment
	how do we show that it behaves according to requirements?
      model checking checks dynamic behavior.
   Chapter 3, sections 3.1 and 3.2