Page 95 - Discrete Mathematics and Its Applications

74 1 / The Foundations: Logic and Proofs

EXAMPLE 7 Show that the premises “If you send me an e-mail message, then I will finish writing the
program,” “If you do not send me an e-mail message, then I will go to sleep early,” and “If I go
to sleep early, then I will wake up feeling refreshed” lead to the conclusion “If I do not finish
writing the program, then I will wake up feeling refreshed.”

Solution: Let p be the proposition “You send me an e-mail message,” q the proposition “I will
finish writing the program,” r the proposition “I will go to sleep early,” and s the proposition “I
will wake up feeling refreshed.” Then the premises are p → q, ¬p → r, and r → s. The desired
conclusion is ¬q → s. We need to give a valid argument with premises p → q, ¬p → r, and
r → s and conclusion ¬q → s.
This argument form shows that the premises lead to the desired conclusion.
Step Reason
1. p → q Premise
2. ¬q →¬p Contrapositive of (1)
3. ¬p → r Premise
4. ¬q → r Hypothetical syllogism using (2) and (3)
5. r → s Premise ▲
6. ¬q → s Hypothetical syllogism using (4) and (5)

Resolution

Computer programs have been developed to automate the task of reasoning and proving theo-
rems. Many of these programs make use of a rule of inference known as resolution. This rule
of inference is based on the tautology

((p ∨ q) ∧ (¬p ∨ r)) → (q ∨ r).

(Exercise30inSection1.3asksfortheverificationthatthisisatautology.)Thefinaldisjunctionin
the resolution rule, q ∨ r, is called the resolvent. When we let q = r in this tautology, we obtain
(p ∨ q) ∧ (¬p ∨ q) → q. Furthermore, when we let r = F, we obtain (p ∨ q) ∧ (¬p) → q
(because q ∨ F ≡ q), which is the tautology on which the rule of disjunctive syllogism is based.

EXAMPLE 8 Use resolution to show that the hypotheses “Jasmine is skiing or it is not snowing” and “It is
snowing or Bart is playing hockey” imply that “Jasmine is skiing or Bart is playing hockey.”

Solution: Let p be the proposition “It is snowing,” q the proposition “Jasmine is skiing,” and r
the proposition “Bart is playing hockey.” We can represent the hypotheses as ¬p ∨ q and p ∨ r,
respectively. Using resolution, the proposition q ∨ r, “Jasmine is skiing or Bart is playing
hockey,” follows. ▲

Resolution plays an important role in programming languages based on the rules of logic,
such as Prolog (where resolution rules for quantified statements are applied). Furthermore, it
can be used to build automatic theorem proving systems. To construct proofs in propositional
logic using resolution as the only rule of inference, the hypotheses and the conclusion must be
expressed as clauses, where a clause is a disjunction of variables or negations of these variables.
We can replace a statement in propositional logic that is not a clause by one or more equivalent
statements that are clauses. For example, suppose we have a statement of the form p ∨ (q ∧ r).
Because p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r), we can replace the single statement p ∨ (q ∧ r) by
two statements p ∨ q and p ∨ r, each of which is a clause. We can replace a statement of
the form ¬(p ∨ q) by the two statements ¬p and ¬q because De Morgan’s law tells us that
¬(p ∨ q) ≡¬p ∧¬q. We can also replace a conditional statement p → q with the equivalent
disjunction ¬p ∨ q.