Formal proof that if a woman weighs the same as a duck, then she must be a witch
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!