Select Answers forExam Prep for COMP 30411 (2007)

Please let Bijan know if there are any typos or other errors. I didn't "show work" here.

Propositional

  1. \(\neg p \rightarrow (\neg q \land (r \land \neg s))\)
    1. \(\{\{\neg p\}, \{q, \neg r, s\}\}\) (remember we negated the above formula!)
    2. There are no matching literals, thus no applications of the resolution rule. Thus there is no way to derive the empty clause and this formula is satisfiable.
    3. We can use tableau either directly on the formulae or on the negation. Here I'm working directly on the formulae and it's pretty trivial (implication and double negation elimination is all you need). \[p \lor (\neg q \land (r \land s))\]
    4. We get a completed branch in one step by applying the OR-rule.