5.11. Summary

Try these first

1. 1.

   Explain the resolution rule in your own words.

   Hint

   Think about how contradictions can lead to simplifications.

2. 2.

   What does the term resolvent refer to?

   Hint

   Consider it the 'output' of the resolution process.

3. 3.

   What does the resolution rule allow us to do?

   • Derive new conclusions
   • Create contradictions
   • Expand clauses
   • None of the above

   Hint

   Consider its purpose in logic.

4. 4.

   True or False: The resolvent is the combined outcome after resolving two clauses.

   Hint

   Recall what happens when we resolve clauses.

5. 5.

   Given the clauses C1: X ∨ Y, C2: ¬X ∨ Z, C3: ¬Z, construct a resolution tree and determine if C4: ¬Y can be concluded.

   Hint

   Focus on all possible resolutions until you exhaust options.

6. 6.

   Formulate a proof by resolution refutation for the premises: P → Q, Q → R and the conclusion ¬R.

   Hint

   Be systematic; step through each resolution carefully.