Skip to main content

Resolution: Tuesday test argument

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.

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".

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.ClauseSource
1¬p ∨ d ∨ mp → (d ∨ m) ≡ ¬p ∨ d ∨ m
2¬s ∨ ¬ms → ¬m
3pfrom p ∧ s
4sfrom p ∧ s
5¬dnegated conclusion

Resolution steps

StepResolventFromResolved on
6d ∨ m1, 3p
7m6, 5d
8¬m2, 4s
9□ (empty clause)7, 8m

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

✓ Answer checked by Claude Opus 5.5 (high effort)

Related questions

All Discrete Structure chapter 1 questions →