---
title: "Resolution: Tuesday test argument"
subject: "Discrete Structure"
chapter: 1
key: "semester_4/discrete_structure:resolution-tuesday-discrete-structure"
source: https://www.bctengineer.com/q/semester_4/discrete_structure/resolution-tuesday-discrete-structure
site: BCT Engineering
---

# Resolution: Tuesday test argument

Discrete Structure · Chapter 1: Logic, Induction and Reasoning

- Asked in: 2072 Asoj, 8 marks
- Video: [Resolution(Rules of Inference of Propositional Logic) | Logic and Proofs | Discrete Mathematics |](https://www.youtube.com/watch?v=otnrBuOpR9E) — MATHS etc.(हिंग्LISH)
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_4/discrete_structure/resolution-tuesday-discrete-structure
- Whole chapter: https://www.bctengineer.com/md/semester_4/discrete_structure/chapter-1

## Question

Using resolution principle, prove that the hypotheses "If today is Tuesday then I will have a test in Discrete Structure or Microprocessor." If my Microprocessor teacher is sick then I will not have a test in Microprocessor." and "Today is Tuesday and my Microprocessor teacher is sick." lead to the conclusion that "I will have a test in Discrete Structure".

## Short answer

Symbolize: p: Tuesday, d: Discrete test, m: Microprocessor test, s: teacher sick. Clauses: ¬p ∨ d ∨ m, ¬s ∨ ¬m, p, s, ¬d. Resolve p with clause 1 to get d ∨ m; resolve with ¬d to get m; resolve s with clause 2 to get ¬m; resolve m and ¬m to yield □, proving d.

## Answer

**Method.** Resolution is a refutation proof. We convert the hypotheses and the negation of the conclusion into clauses and derive the empty clause (□).

#### Propositions
- p: today is Tuesday
- d: I will have a test in Discrete Structure
- m: I will have a test in Microprocessor
- s: my Microprocessor teacher is sick

#### Hypotheses in symbols
1. p → (d ∨ m)
2. s → ¬m
3. p ∧ s

Conclusion: d. We add its negation ¬d.

#### Clauses (CNF)
| No. | Clause | Source |
|---|---|---|
| 1 | ¬p ∨ d ∨ m | p → (d ∨ m) ≡ ¬p ∨ d ∨ m |
| 2 | ¬s ∨ ¬m | s → ¬m |
| 3 | p | from p ∧ s |
| 4 | s | from p ∧ s |
| 5 | ¬d | negated conclusion |

#### Resolution steps
| Step | Resolvent | From | Resolved on |
|---|---|---|---|
| 6 | d ∨ m | 1, 3 | p |
| 7 | m | 6, 5 | d |
| 8 | ¬m | 2, 4 | s |
| 9 | □ (empty clause) | 7, 8 | m |

The empty clause is derived, so the set {hypotheses, ¬d} is unsatisfiable. Therefore the hypotheses imply "I will have a test in Discrete Structure". ∎

## Check yourself

The answer's key points as multiple-choice questions, with the correct option and why.

1. What does a resolution proof do with the conclusion?
   A. Resolves it with itself
   B. Adds its negation to the clauses and derives the empty clause
   C. Adds it to the clauses and derives the same clause
   D. Removes it from the hypotheses
   Answer: B. Resolution is refutation: add ¬conclusion and derive □. (Key point: Refutation idea)

2. p → (d ∨ m) becomes which clause?
   A. p ∨ d ∨ m
   B. ¬p ∨ d ∨ m
   C. ¬p ∧ (d ∨ m)
   D. ¬p ∨ ¬d ∨ ¬m
   Answer: B. A → B ≡ ¬A ∨ B, giving ¬p ∨ d ∨ m. (Key point: CNF conversion)

3. Resolving d ∨ m with ¬d gives which clause?
   A. d
   B. m
   C. □
   D. ¬m
   Answer: B. Resolving on d cancels d and ¬d, leaving m. (Key point: Resolving)

4. Which pair of clauses finally gives □?
   A. p and s
   B. m and ¬m
   C. d and ¬d
   D. ¬s and ¬m
   Answer: B. Clause 7 (m) and clause 8 (¬m) resolve on m to give the empty clause. (Key point: Empty clause)

## Related in Discrete Structure

- [Rules of inference: Sunday test in MFC](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-sunday-test) — Discrete Structure, chapter 1
- [Rules of inference: cheque book argument](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-cheque-book) — Discrete Structure, chapter 1
- [Rules of inference: Randy and the job](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-randy-job) — Discrete Structure, chapter 1
- [Rules of inference: sailing race](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-sailing-race) — Discrete Structure, chapter 1
- [Rules of inference: e-mail and program](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-email-program) — Discrete Structure, chapter 1
- [Rules of inference: movie and sunset](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-rainy-movie) — Discrete Structure, chapter 1

## Related in other subjects

- [Discrete vs continuum structure; stability](https://www.bctengineer.com/question.md?key=semester_1%2Fapplied_mechanics%3Adiscrete-continuum-structure-stability-determinacy) — Applied Mechanics, chapter 6
- [Resolution: Mary loves John](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-mary-john-football) — Artificial Intelligence, chapter 4
- [XML and DTD; Teacher XML document](https://www.bctengineer.com/question.md?key=semester_7%2Fweb_technology%3Axml-teacher-dtd) — Web Technology, chapter 7, asked 2×
- [Transmission and y parameters, prove not reciprocal or symmetrical](https://www.bctengineer.com/question.md?key=semester_3%2Felectrical_circuit_theory%3Atransmission-and-y-parameters-neither-reciprocal) — Electrical Circuit Theory, chapter 7, asked 2×