Formal proof that if a woman weighs the same as a duck, then she must be a witch

Posted: June 7th, 2004 | Filed under: Uncategorized | No Comments »

One of the best things about languages such as Prolog is the ease with which you can validate theorums. As an example take a look at the program to validate the theory that if a woman weighs the same as a duck, then she must be a witch:

witch(X)  <= burns(X) and female(X).
burns(X)  <= wooden(X).
wooden(X) <= floats(X).
floats(X) <= sameweight(duck, X).

female(girl).          {by observation}
sameweight(duck,girl). {by experiment }

? witch(girl).
> yes

For reference here is the original plain english line of reasoning:

BEDEVERE:
    Quiet! Quiet! Quiet! Quiet! There are ways of telling whether she is a witch.
VILLAGER #1:
    Are there?
VILLAGER #2:
    Ah?
VILLAGER #1:
    What are they?
CROWD:
    Tell us! Tell us!...
VILLAGER #2:
    Do they hurt?
BEDEVERE:
    Tell me. What do you do with witches?
VILLAGER #2:
    Burn!
VILLAGER #1:
    Burn!
CROWD:
    Burn! Burn them up! Burn!...
BEDEVERE:
    And what do you burn apart from witches?
VILLAGER #1:
    More witches!
VILLAGER #3:
    Shh!
VILLAGER #2:
    Wood!
BEDEVERE:
    So, why do witches burn?
    [pause]
VILLAGER #3:
    B--... 'cause they're made of... wood?
BEDEVERE:
    Good! Heh heh.
CROWD:
    Oh, yeah. Oh.
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.
RANDOM:
    Oh, yeah. True. Uhh...
BEDEVERE:
    Does wood sink in water?
VILLAGER #1:
    No. No.
VILLAGER #2:
    No, it floats! It floats!
VILLAGER #1:
    Throw her into the pond!
CROWD:
    The pond! Throw her into the pond!
BEDEVERE:
    What also floats in water?
VILLAGER #1:
    Bread!
VILLAGER #2:
    Apples!
VILLAGER #3:
    Uh, very small rocks!
VILLAGER #1:
    Cider!
VILLAGER #2:
    Uh, gra-- gravy!
VILLAGER #1:
    Cherries!
VILLAGER #2:
    Mud!
VILLAGER #3:
    Uh, churches! Churches!
VILLAGER #2:
    Lead! Lead!
ARTHUR:
    A duck!
CROWD:
    Oooh.
BEDEVERE:
    Exactly. So, logically...
VILLAGER #1:
    If... she... weighs... the same as a duck,... she's made of wood.
BEDEVERE:
    And therefore?
VILLAGER #2:
    A witch!