Assignment 1: Assigned September 8, due Monday, September 15 at 8:30am

1. Briefly describe the advantages of formal specification of systems. At what stages of the system development cycle is formal specification useful?

2. p.78, 1.1 (1ij) Use ~ (negation), ->, /\, and \/ to express the following declarative sentence in propositional logic; state what your respective propositional atoms p, q, etc. mean:

   (i) If Dick met Jane yesterday, they had a cup of coffee together, or they took a walk in the park.

   (j) No shoes, no shirt, no service. (Please note that this means that the dress code of an establishment such as a restaurant is that all people who enter must be wearing both shoes and a shirt. Anyone who is not will not be served by the restaurant.)

3. p.79, 1.2 (1c) Prove the sequent (p /\ q) /\ r |- p /\ (q /\ r)

4. p.79, 1.2 (1e) Prove the sequent q -> (p -> r), ~r, q |- ~p

5. p.79, 1.2 (1l) Prove the sequent p -> q, r -> s |- p \/ r -> q \/ s

6. p.79, 1.2 (1m) Prove the sequent p \/ q |- r -> (p \/ q) /\ r

7. p.81, 1.3 (2b) For the formula below, list all its subformulas. Hint: it may help to draw the parse tree first.
   (s -> r \/ l) \/ (~q /\ r) -> (~(p -> s) -> r)

8. Extra credit: p.79, 1.2 (2i)