Columbia University Department of Computer Science

(original, maybe, science)

My officemate is the TA for Artificial Intelligence, and today he was explaining Resolution Theorem Proving using Predicate Calculus to a bunch of students. They were looking for an example, so I suggested they use Sir Bedevere's proof that the girl the villagers were trying to burn was, indeed, a witch (in "Monty Python and the Holy Grail"). They thought it would take too long, but I worked out the proof anyway. Without repeating the dialog (which is a copyrighted work, but at least one person at your site should be able to recite it by heart!), here are Sir Bedevere's arguments, expressed in Predicate Calculus (only those pertinent to the proof are included. Let us not worry about the truth of some of these implications). [1] BURNS(x) /\ WOMAN(x) => WITCH(x) [2] WOMAN(GIRL) [3] \forall x, ISMADEOFWOOD(x) => BURNS(x) [4] \forall x, FLOATS(x) => ISMADEOFWOOD(x) [5] FLOATS(DUCK) [6] \forall x,y FLOATS(x) /\ SAMEWEIGHT(x,y) => FLOATS(y) and, by experiment [7] SAMEWEIGHT(DUCK,GIRL) Now, remember how we do resolution; we refute the statement we try to prove and try to resolve the statemets to nil (false). The way we do that is by putting the statements in Conjunctive Normal Form (a list of statements whose terms are connected with logical or's), and then using pairs of statements where a term appears in both affirmative and negated form, and resolving. For more information on RTP, consult any AI textbook. First, we reduce [1] through [7] to Conjunctive Normal Form [1] yields ~(BURNS(x) /\ WOMAN(x)) \/ WITCH(x) which yields [9] ~BURNS(x) \/ ~WOMAN(x) \/ WITCH(x) [3] yields [10] ~ISMADEOFWOOD(x) \/ BURNS(x) [4] yields [11] ~FLOATS(x) \/ ISMADEOFWOOD(x) [6] yields ~(FLOATS(x) /\ SAMEWEIGHT(x,y)) \/ FLOATS(y) which yields [12] ~FLOATS(x) \/ ~SAMEWEIGHT(x, y) \/ FLOATS(y) Now we are trying to prove WITCH(GIRL), so we add [13] ~WITCH(GIRL) and we'll try to resolve these statements to a NIL. ------------ Substituting DUCK and GIRL for x and y in [12] we get: [14] ~FLOATS(DUCK) \/ ~SAMEWEIGHT(DUCK, GIRL) \/ FLOATS(GIRL) which we resolve with [7] to get [15] ~FLOATS(DUCK) \/ FLOATS(GIRL) which we resolve with [5] to get [16] FLOATS(GIRL) We substitute GIRL for x in [11] and we get [17] ~FLOATS(GIRL) \/ ISMADEOFWOOD(GIRL) which we resolve with [16] to get [18] ISMADEOFWOOD(GIRL) We substitute GIRL for x in [10] to get [19] ~ISMADEOFWOOD(GIRL) \/ BURNS(GIRL) which we resolve with [18] to get [20] BURNS(GIRL). Now we substitute GIRL for x in [9] to get [21] ~BURNS(GIRL) \/ ~WOMAN(GIRL) \/ WITCH(GIRL) which we resolve with [20] to get [22] ~WOMAN(GIRL) \/ WITCH(GIRL) which we resolve with [2] to get [23] WITCH(GIRL) which we resolve with [13] to get NIL, which proves, once and for all, that the villagers were right and the girl was indeed a witch! BURN HER! /ji In-Real-Life: John "Heldenprogrammer" Ioannidis E-Mail-To: ji@cs.columbia.edu V-Mail-To: +1 212 854 8120 P-Mail-To: 450 Computer Science \n Columbia University \n New York, NY 10027

(From the "Rest" of RHF)