2022-CS357FZ-January
Q1
(a) Explain Design by Contract in terms of the roles of client and supplier. In your explanation, you need to mention the following concepts: 1. Preconditions 2. Post conditions 3. Roles of the client 4. Roles of the supplier 5. Benefits of design by contract
- Design by Contract (DbC) is a software design approach that establishes a formal agreement between the client and the supplier.
- It involves specifying preconditions (requirements before using a function) and postconditions (expected outcomes after using a function).
- Clients must satisfy preconditions, and suppliers must ensure postconditions.
- DbC enhances software reliability, clarity, and robustness, aiding debugging.
(b) Use natural deduction rules to prove the validity of the following formulas.
1 | x3→x2 | premise |
2 | x2→x5 | premise |
3 | x3∨(x4∧x1) | premise |
4 | x3 | assumption (分支1) |
5 | x2 | →e 1,4 |
6 | x5 | →e 2,5 |
7 | x4∨x5 | ∨i 6 |
8 | (x4∧x1) | assumption (分支2) |
9 | x4 | ∧e 8 |
10 | x4∨x5 | ∨i 9 |
11 | x4∨x5 | ∨3, 4-7, 8-10 |
1 | ∃x(Q(x)) | premise |
2 | ∀x(Q(x)→P(x)) | premise |
3 | a Q(a) | ∃ i 1 |
4 | Q(a) → P(a) | ∀e 2 |
5 | P(a) | →e 4,3 |
6 | ∃x(P(x)) | ∃ i 5 |
(c) Precisely explain the difference between propositional logic and predicate logic. Provide examples to support your answer.
- Propositional Logic uses simple statements, which can either be true or false.
Examples - If it is raining, then the ground is wet:
It is raining → The ground is wet- Predicate Logic introduces the use of quantifiers ∀ / ∃ and variables.
Examples - All humans are mortal:
∀x (Human(x) → Mortal(x))Q2
(b) Convert the following formula to CNF
2023-CS357FZ-January
Q2
(a) By employing Natural Deduction rules in propositional logic, prove the following theorem.
1 | X∧(Y∨¬Z) | premise |
2 | X | ∧e 1 |
3 | Y∨¬Z | ∧e 1 |
4 | Y | assumption |
5 | X∧Y | ∧i 2,4 |
6 | (X∧Y)∨(X∧¬Z) | ∨i 5 |
7 | ¬Z | assumption |
8 | X∧¬Z | ∧i 2,7 |
9 | (X∧Y)∨(X∧¬Z) | ∨i 8 |
10 | (X∧Y)∨(X∧¬Z) | ∨e 3, 4-6, 7-9 |
(c) By employing natural deduction rules in First Order Logic, prove the following theorems.
1 | P(t) | premise |
2 | ∀x(P(x)→¬Q(x)) | premise |
3 | t0 P(t0)→¬Q(t0) | ∀ e 1, 2 |
4 | ¬Q(t0) | → e 1, 3 |
1 | ∀x(∃y(P(x)→Q(y)) | premise |
2 | a ∃y(P(a)→Q(y)) | ∀ e 1 |
3 | ∃x∃y(P(x)→Q(y)) | ∃ i 2 |
Q3
(a) Convert the following formula to CNF form by employing the approach of introducing a new variable during the translation
Lab Review
Lab 8In the case of each of the following, decide whether or not the deduction is valid. If it is valid give a natural deduction proof; if not, provide a model in which it does not hold.
This is valid.
1 | y0 | assumption |
2 | (∀xP(x) → P(y0) | substitution of ∃y with yo |
3 | P(y0) | ∀ e 2 |