Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Resolution - The Resolution Rule

  • When the two initial clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair

    • However, only the pair of literals that are resolved upon can be removed: All other pairs of literals remain in the resolvent clause

  • Modus ponens (see last lecture) can be seen as a special case of resolution of a one-literal clause and a two-literal clause

  • Example: Given clauses

    • P(x, f(a)) v P(x, f(y)) v Q(y) and ¬P(z, f(a)) v ¬ Q(z)

    • P(x, f(a)) and ¬P(z, f(a)) unify with substitution σ = {x/z}

    • Therefore, we derive the resolvent clause (to which σ is applied):

    • P(z, f(y)) v Q(y) v ¬ Q(z)

Speaker notes:

Content Tools


There are currently no sources for this slide.