CSC 8520-001 Artificial Intelligence: Burn the Witch!
Wednesdays from 6:15pm to 8:45pm in Mendel G29
Dr. David Matuszek, Mendel 162C, (610) 519-5654
Villanova University, Spring 2000

This is slightly adapted from John Ioannidis's original, which can be found at http://www.netfunny.com/rhf/jokes/90q4/burnher.html


Monty Python and the Holy Grail
Scene 5: 'Burn the witch!'
(abridged)

BEDEVERE: Quiet! Quiet! Quiet! Quiet! There are ways of telling whether she is a witch.

CROWD: Tell us! Tell us!...

BEDEVERE: Tell me. What do you do with witches?

CROWD: Burn! Burn them up! Burn!...
[1] BURNS(x) AND WOMAN(x) => WITCH(x)

[2] WOMAN(GIRL)
BEDEVERE: And what do you burn apart from witches?

VILLAGER #1: More witches!

VILLAGER #2: Wood!

BEDEVERE: So, why do witches burn?

VILLAGER #3: B--... 'cause they're made of... wood?

BEDEVERE: Good! Heh heh.

 [3] FOR ALLx, ISMADEOFWOOD(x) => BURNS(x)
BEDEVERE: So, how do we tell whether she is made of wood?

VILLAGER #1: Build a bridge out of her.

BEDEVERE: Ah, but can you not also make bridges out of stone?

VILLAGER #1: Oh, yeah.

BEDEVERE: Does wood sink in water?

VILLAGER #2: No, it floats! It floats!

CROWD: The pond! Throw her into the pond!

 [4] FOR ALLx, FLOATS(x) => ISMADEOFWOOD(x)
BEDEVERE: What also floats in water?

VILLAGER #3: Uh, very small rocks!

ARTHUR: A duck!

CROWD: Oooh.

 [5] FLOATS(DUCK)
BEDEVERE: Exactly. So, logically...

VILLAGER #1: If... she... weighs... the same as a duck,... she's made of wood.

BEDEVERE: And therefore?

CROWD: A witch! A witch!...

 [6] FOR ALLx,y FLOATS(x) AND SAMEWEIGHT(x,y) => FLOATS(y)
VILLAGER #4: Here is a duck. Use this duck.

DUCK: [quack quack quack]

BEDEVERE: Very good. We shall use my largest scales.

BEDEVERE: Right. Remove the supports!

[whop] [clunk] [creak]

CROWD: A witch! A witch! A witch!

WITCH: It's a fair cop.

CROWD: Burn her! Burn her! Burn her! Burn! Burn!...

 and, by experiment,

[7] SAMEWEIGHT(DUCK,GIRL)

First, we reduce [1] through [7] to Conjunctive Normal Form

From: We get:
[1] BURNS(x) AND WOMAN(x) => WITCH(x) [9] NOTBURNS(x) OR NOTWOMAN(x) OR WITCH(x)
[2] WOMAN(GIRL)  
[3] FOR ALLx, ISMADEOFWOOD(x) => BURNS(x) [10] NOTISMADEOFWOOD(x) OR BURNS(x)
[4] FOR ALLx, FLOATS(x) => ISMADEOFWOOD(x) [11] NOTFLOATS(x) OR ISMADEOFWOOD(x)
[5] FLOATS(DUCK)  
[6] FOR ALLx,y FLOATS(x) AND SAMEWEIGHT(x,y) => FLOATS(y) NOT(FLOATS(x) AND SAMEWEIGHT(x,y)) OR FLOATS(y) -- that is,
[12] NOTFLOATS(x) OR NOTSAMEWEIGHT(x, y) OR FLOATS(y)
[7] SAMEWEIGHT(DUCK,GIRL)  
To prove: WITCH(GIRL) So add:
[13] NOTWITCH(GIRL)

Now we'll try to resolve these statements to a NIL.

Using: Conclude:
[12] NOTFLOATS(x) OR NOTSAMEWEIGHT(x, y) OR FLOATS(y) Substituting DUCK and GIRL for x and y gives:
[14] NOTFLOATS(DUCK) OR NOTSAMEWEIGHT(DUCK, GIRL) OR FLOATS(GIRL)
[14] NOTFLOATS(DUCK) OR NOTSAMEWEIGHT(DUCK, GIRL) OR FLOATS(GIRL)
[7] SAMEWEIGHT(DUCK,GIRL)		 [15] NOTFLOATS(DUCK) OR FLOATS(GIRL)
[15] NOTFLOATS(DUCK) OR FLOATS(GIRL)
[5] FLOATS(DUCK)
 [16] FLOATS(GIRL)
[11] NOTFLOATS(x) OR ISMADEOFWOOD(x) Substituting GIRL for x gives:
[17] NOTFLOATS(GIRL) OR ISMADEOFWOOD(GIRL)
[17] NOTFLOATS(GIRL) OR ISMADEOFWOOD(GIRL)
[16] FLOATS(GIRL)		 [18] ISMADEOFWOOD(GIRL)
[10] NOTISMADEOFWOOD(x) OR BURNS(x) Substituting GIRL for x gives:
[19] NOTISMADEOFWOOD(GIRL) OR BURNS(GIRL)
[19] NOTISMADEOFWOOD(GIRL) OR BURNS(GIRL)
[18] ISMADEOFWOOD(GIRL)		 [20] BURNS(GIRL)
[9] NOTBURNS(x) OR NOTWOMAN(x) OR WITCH(x) Substituting GIRL for x gives:
[21] NOTBURNS(GIRL) OR NOTWOMAN(GIRL) OR WITCH(GIRL)
[20] BURNS(GIRL)
[21] NOTBURNS(GIRL) OR NOTWOMAN(GIRL) OR WITCH(GIRL)		 [22] NOTWOMAN(GIRL) OR WITCH(GIRL)
[22] NOTWOMAN(GIRL) OR WITCH(GIRL)
[2] WOMAN(GIRL)		 [23] WITCH(GIRL)
[23] WITCH(GIRL)
[13] NOTWITCH(GIRL)		 NIL
which proves, once and for all, that the villagers were right and the girl was indeed a witch! BURN HER!