Resolution in Monty Python
Fall 2015, 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] ¬ [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!