PowerPoint Presentation
Resolution
¬A ∨ B ∨ E, ¬B ∨ ¬D, C ∨ A, ¬C, D, ¬E
Apply resolution to this (set/conjunction of) clauses
Which sequence(s) may be generated amongst
¬A ∨ E ∨ ¬D, E ∨ ¬D ∨ C, ¬D ∨ C , C,
B ∨ E ∨ C , E ∨ ¬D ∨ C, ¬D ∨ C , C,
E ∨ ¬D ∨ C, ¬D ∨ C , B ∨ E ∨ C ∨ A, C,
Resolution
¬A ∨ B ∨ E, ¬B ∨ ¬D, C ∨ A, ¬C, D, ¬E
• Resolution with ¬A ∨ B ∨ E and ¬B ∨ ¬D gives ¬A ∨ E ∨ ¬D
• Resolution with ¬A ∨ E ∨ ¬D and C ∨ A gives E ∨ ¬D ∨ C
• Resolution with E ∨ ¬D ∨ C and ¬E gives ¬D ∨ C
• Resolution with ¬D ∨ C and D gives C
• Resolution with C and ¬C gives
Thus the sequence ¬A ∨ E ∨ ¬D, E ∨ ¬D ∨ C, ¬D ∨ C , C, may be
generated by applying resolution
Resolution
¬A ∨ B ∨ E, ¬B ∨ ¬D, C ∨ A, ¬C, D, ¬E
• Resolution with ¬A ∨ B ∨ E and C ∨ A gives B ∨ E ∨ C
• Resolution with B ∨ E ∨ C and ¬B ∨ ¬D gives E ∨ ¬D ∨ C
• Resolution with E ∨ ¬D ∨ C and ¬E gives ¬D ∨ C
• Resolution with ¬D ∨ C and D gives C
• Resolution with C and ¬C gives
Thus the sequence B ∨ E ∨ C , E ∨ ¬D ∨ C, ¬D ∨ C , C, may be
generated by applying resolution