Resolution Theorem Proving

• Proof by contradiction: If we negate the formula to be proven and add this to a consistent database of axioms, the database will contain a contradiction if and only if the formula is true.
• Resolution algorithm

  To prove a formula P given a set of axioms A

  • Negate P and add it to A.
  • Convert all of the formulas (included the negated goal) to clause form.
  • Until a contradiction (empty clause) has been found, or there is no resolvable pair of clauses, or some predetermined amount of effort has been expended,
    • Select two resolvable clauses.
    • Resolve them together. If the resolvent is the empty clause, a contradiction has been found. Otherwise add the resolvent to A.
• If the goal is an information question (a fill-in-the-blank question, one with what?, where?, etc.), there is some argument in a formula Q representing the question which corresponds to a variable. Instead of the negation of the goal formula, add a formula to the database which asserts that if Q is true, then that variable will be the "answer". For example, to find out where Wanda lives, you might add the following:

  (lives wanda ?x) -> (answer ?x)
  

  When converted to clause form, this becomes

  (~ (lives wanda ?x)) V (answer ?x)
  

  In this case you terminate the procedure when resolving two clauses results in a clause consisting only of an answer predicate.