This exercise uses logical notation, not computer science notation. In the notation/terminology used in the “Propositional Logic” handout for ISC321 the disjunctions a ∨ b ∨ c ∨ ¬e , b ∨ ¬c ∨ d ∨ f and ¬b are the three clauses {a, b, c, ¬e} , { b, ¬c, d, f } and {¬b}, that make up the formula { {a, b, c, ¬e} , { b, ¬c, d, f } , {¬b} }. Resolution then operates on pairs of clauses, ‘inside the formula’, by cancellation of single literals. Note that a formula like { {a, ¬a }, {a, ¬a, b } } is always true (contains no information!) and resolution only yields { {a, ¬a, b } } (no info!). We do not and we cannot and we must not conclude { b } from this!
Resolution is a logical operation on two disjunctions (propositions linked by ‘or’: a or b or c or…) that allows you to cancel one single contradicting member from each disjunction while joining the rest together. Here is a (slightly messy example):
The more complicated versions (with long disjunctions) lead to correct conclusions (are sound) because c cannot be true and false at the same time; it cannot be that both assumptions are true, one ‘because of c’ and the other ‘because of ¬c’. So one of the disjunctions from the ‘rest’ (the one without c or the one without ¬c) must be true (if the assumptions are). So the resolvent is true, if the original two clauses (assumptions) are, because it contains both rests.
Question 1 An eminently practical and useful application of resolution: Analyze the English sentences below, express their logical essence as disjunctions (or single propositions) and prove, using resolution, Conclusion (C1) from the Assumptions (A1).
Assumptions (A1): If I do not drink beer and work hard, I will be promoted.
I was not promoted, although I worked hard.
Conclusion (C1): I drank beer.
Further instructions: use the letters d, w, and p to mean ‘I drink beer’, ‘I worked hard’, and ‘I was promoted’.
Draw a tree as suggested by the example (your tree should have three levels, as the example).
Hints: ‘although’ has no logical content beyond ‘and’. The second assumption will thus be represented as two separate single propositions: ¬p and w. Note that a → b (if a then b) is equivalent to ¬a ∨ b and thus the first assumption is the same as ‘I drink beer’ or ‘I do not work hard’ or ‘I will be promoted’. Don’t worry about tense: drink/drank, it’s all the same.
Question 2: Use the same method to formalize the following assumptions and presumed conclusion. Try to use the resolution and see what happens. Explain what is going on here.
Assumptions (A2): If I play golf with the boss (g) and work overtime (o), I will get more
money (m). I worked overtime and I got more money.
Conclusion (C2): I played golf with the boss.
Instruction and hints: See Question 1. Start drawing the tree. For the explanation apply the observation that, for instance, the truth of ‘a implies b’ and ‘b’ does not mean that ‘a’ must be true. For instance: If I have a bicycle, I bicycle to school. I bicycle to school. But on my friend’s bicycle (and I don’t have one!). Explain how this applies to the situation in Question 2. So, can we be sure that I played golf with the boss??
