An Example of Answer Extraction

  • Mary is a sister of John.
  • If one person is a sister of the other, then one is a sibling of the other.
  • The father of John is Sam.
  • If one person is a sibling of another, then the father of one is also the father of the other.
  • Who is the father of Mary?
    Express question as an assertion of existence:

    (exists x) Father(x, Mary).

    Express premises in logic and convert to clause form...

    Note that we have not represented the fact that the sibling relation is symmetric.

  • C1: Sister(Mary, John).
  • C2: ~Sister(x1, y1) V Sibling(x1, y1).
  • C3: ~Sibling(x2, y2) V ~Father(z, y2) V Father(z, x2).
  • C4: Father(Sam, John).
  • C5: ~Father(x3, Mary).
    Now apply resolution to derive the null clause from C1-C5.

  • C6 (resolve C1, C2 with { Mary/x1, John/y1}): Sibling(Mary, John).
  • C7 (resolve C3, C6 with { Mary/x2, John/y2}): ~Father(z, John) V Father(z, Mary).
  • C8 (resolve C4, C7 with { Sam/z}): Father(Sam, Mary).
  • C9 (resolve C5, C8 with { Sam/x3}): []

    Although C8 seems to give us our answer, we generally cannot rely on an arbitrarily selected clause from the derivation, because it might be partially derived from the negation of the conclusion. (However, in this example it actually is not.)

    So, in general, we simply perform the following... Change the extra premise ~Father(x3, Mary) into a tautology:

    C5': ~Father(x3, Mary) V Father(x3, Mary).

    Now reapply the same resolution steps as before to the modified set of clauses.

  • C6' (resolve C1, C2 with { Mary/x1, John/y1}): Sibling(Mary, John).
  • C7' (resolve C3, C6' with { Mary/x2, John/y2}): ~Father(z, John) V Father(z, Mary).
  • C8' (resolve C4, C7' with { Sam/z}): Father(Sam, Mary).
  • C9' (resolve C5', C8' with { Sam/x3}): Father(Sam, Mary).

    The answer is given by C9' which is the new clause that corresponds to the clause in the original derivation that represented the contradiction.