Contact
Teaching
 |
 |
|
| Model-Checking SS 2011 | ||
 |
 |
| News | Basic information | Content | Exercises | Slides | Links |
Exercise 1: May 2 (discussion on May 5)
- Recap of logic. Read Tom Henzinger's "How To Write a Proof" and Sections 1.1 - 1.6 in this book (PDF).
- Prove or give a counterexample: ((∀ y: P(y)) ∨ (∀ z: Q(z))) → (∀ x: P(x) ∨ Q(x)).
- Prove or give a counterexample: (∀ x: P(x) ∨ Q(x)) → ((∀ y: P(y)) ∨ (∀ z: Q(z))).
- Read (PDF). Prove a dual of Theorem 2, i.e., prove that if a node is reachable then it will be an element of the set C.