MUN Computer Science 1002 - Lab 2

Proofs in propositional logic

Review:

• Unit 2.

Vocabulary

• argument, valid/invalid argument, natural deduction, rules of inference, modus ponens, premises, conclusion
• Resolution rule, refutation

Remember that the goal of this activity is not just to solve the puzzle, but practice translating from English to logic, writing valid arguments using natural deduction rules, and verifying arguments by doing a resolution refutation. Make sure all of the members of your group know how to do all the steps.

Where is the iceberg?

Imagine that it is a nice sunny day in late May, and you have a friend visiting from out of province. Your friend says: "I read yesterday on CBC that people taking boat tours could see a beautiful iceberg not too far away from St. John's, and that it might be visible there from the shore today". Now, you are thinking: if it is not too far from St. John's, it could be at Flatrock, Middle Cove, Petty Harbour or Cape Spear. The tour boats go either from St. John's or from Bay Bulls. The tour boats from St. John's go to Middle cove as well as to Petty Harbour, but not to Flatrock and not to Cape Spear. Tour boats from Bay Bulls may go only to Cape Spear. As the iceberg moves south, it would pass Flatrock, then Middle Cove, then Petty Harbour, then Cape Spear. If it got as far south as Petty Harbour or Cape Spear, it would have been visible from St. John's Signal Hill yesterday, unless it was foggy. If it were visible from Signal hill, that would surely be mentioned in that CBC article, but sounds like it wasn't. It was not foggy at all yesterday.

In this exercise, you will use logic (in particular natural deduction and resolution) to figure out where to take your friend to see the iceberg.

1. List all propositions in this question that are relevant for finding the iceberg, and give each a name you could use in a formula. For example, you might want to have propositions $p_2:$ "the iceberg was seen from a Bay Bulls tour boat" and $q_4$: "the iceberg is at Cape Spear", but you would not need a proposition for "the iceberg is beautiful".
2. Using these propositions, write logic formulas for all the relevant facts mentioned above. For example, you might have a formula for "If the iceberg was seen from a Bay Bulls tour boat, then it must be at Cape Spear" as one of the facts, which you would write as $(p_2 \to q_4)$ using propositions from the previous subquestion.
3. Using rules of natural deduction such as modus ponens, derive from these facts the location of the iceberg. Say to which formulas each rule is applied, and what you derive at each step.

   You can simplify individual premises and intermediate derived formulas using logical equivalences such as De Morgan's law, take contrapositives of implications and convert disjunction to implications. Hint: in addition to modus ponens and its "friends" modus tollens (modus ponens on contrapositive) and disjunctive syllogism (modus ponens on OR converted to implication), you might find auxiliary rules such as deriving $A$ (or, similarly, $B$) from $A \wedge B$ (called "simplification" in the textbook), deriving $A \vee B$ from $A$ ("weakening rule") and deriving $A \wedge B$ from premises $A$ and $B$ ("conjunction rule") useful. The only other rule in the textbook, except for resolution, is the hypothetical syllogism that lets you derive $p \to r$ from $p \to q$ and $q \to r$. You should not need any other rules.

4. Now let's check your reasoning using resolution refutation. First, convert each premise into CNF form (as well as negation of the conclusion). Hint: remember that $A \vee (B \wedge C) \equiv (A \vee B) \wedge (A \vee C)$ for any logic formulas $A, B, C$.
5. Now, write a CNF formula for "AND of premises AND NOT conclusion".
6. Finally, do a resolution refutation on the resulting formula to check that your argument in part 3 of this question was valid.