Description

Part I, Formal logic: Provide formal proofs, as illustrated in the class notes, for the following theorems:
1. ((P ⇒ R) ∧ (Q ⇒ S)) ⇒ ((P ∧ Q) ⇒ (R ∧ S))
2. (P ⇒ (Q ⇒ R)) ⇒ (Q ⇒ (P ⇒ R)) 3. (P ⇒ (P ⇒ Q)) ⇒ (P ⇒ Q)
4. ((P ⇒ Q) ⇒ Q) ⇒ ((Q ⇒ P) ⇒ P)
5. (P ⇒ Q) ∨ (Q ⇒ P)
6. ((P ⇒ R) ∨ (Q ⇒ R)) ⇒ (P ∧ Q ⇒ R)
7. (P ∧ Q ⇒ R) ⇒ ((P ⇒ R) ∨ (Q ⇒ R))
Part II, Axiomatic Semantics: Provide formal proofs of the following triples.
8. {x > 5}x = 2 * x{x > 8}
9. {y > 0}if x > y then y = x + y{y > 0}
Part III, Concurrency:
10. Provide a formal proof of the following. Show both the annotated code, and proofs of all necessary triples.
{x = 2 ∧ y = 3} co x = y; // y = 4; oc
{x = 3 ∨ x = 4}
1
I provide here an example using the natural deduction package for LATEX. Further examples are in the lectures.
Prove: (P ⇒ Q) ⇒ ((P ∧ R) ⇒ (Q ∧ R))
P ⇒ Q
P ∧ R
P
R
Q
Q ∧ R
(P ∧ R) ⇒ (Q ∧ R)
1.assumption for conditional proof
2.assumption for conditional proof
3.2, simplification
4.2, simplification
5.1, 3, modus ponens
6.4, 5, conjunction
7.conditional proof
8. (P ⇒ Q) ⇒ ((P ∧ R) ⇒ (Q ∧ R)) conditional proof
2