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)
[10] ¬ISMADEOFWOOD(x) ∨ BURNS(x) Substituting GIRL for x gives:
[19] ¬ISMADEOFWOOD(GIRL) ∨ BURNS(GIRL)
[19] ¬ISMADEOFWOOD(GIRL) ∨ BURNS(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!