Resolution in Monty Python
Fall 2011, David Matuszek

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) ∧ 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] ∀x, 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] ∀x, 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] ∀x,y FLOATS(x) ∧ 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) ∧ WOMAN(x) ⇒ WITCH(x) [9] ¬BURNS(x) ∨ ¬WOMAN(x) ∨ WITCH(x)
[2] WOMAN(GIRL)  
[3] ∀x, ISMADEOFWOOD(x) ⇒ BURNS(x) [10] ¬ISMADEOFWOOD(x) ∨ BURNS(x)
[4] ∀x, FLOATS(x) ⇒ ISMADEOFWOOD(x) [11] ¬FLOATS(x) ∨ ISMADEOFWOOD(x)
[5] FLOATS(DUCK)  
[6] ∀x,y FLOATS(x) ∧ SAMEWEIGHT(x,y) ⇒ FLOATS(y) ¬(FLOATS(x) ∧ SAMEWEIGHT(x,y)) ∨ FLOATS(y) -- that is,
[12] ¬FLOATS(x) ∨ ¬SAMEWEIGHT(x, y) ∨ FLOATS(y)
[7] SAMEWEIGHT(DUCK,GIRL)  
To prove: WITCH(GIRL) So add:
[13] ¬WITCH(GIRL)

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

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