```""" "She's a witch!" from Monty Python and the Holy Grail, for the FLiP proof checker. excerpt at http://www.youtube.com/watch?v=zrzMhU_4m-g transcript at http://www.sacred-texts.com/neu/mphg/mphg.htm """ from fol_session import * from villagers import * # "There are ways of telling whether she's a witch." witch_axioms = \ [(Text("She's a witch!"), comment), # "What do you do with witches?" "Burn them!" (A(x, Impl(Witch(x),Burn(x))), given), # "Why do witches burn?" "'Cause they're made of wood!" (A(x, Impl(Wood(x),Witch(x))), given), # "How do we tell if she's made of wood?" # "Does wood sink in water?" "It floats!" (A(x, Impl(Floats(x),Wood(x))), given), # "What also floats in water?" "A duck!" (Floats(duck), given), # "Exactly! So, logically ..." # "If she weights the same as a duck, she's made of wood!" (A(x, A(y, Impl(And(Floats(x),Equal(weight(x),weight(y))),Floats(y)))), given), # "We shall use my largest scales. ... Remove the supports!" (Equal(weight(duck),weight(girl)), given)] check_proof(witch_axioms) rapply(Ae,5,duck) rapply(Ae,7,girl) rapply(ai,4,6) rapply(imple,8,9) rapply(Ae,3,girl) rapply(imple,11,10) rapply(Ae,2,girl) rapply(imple,13,12) rapply(Ae,1,girl) rapply(imple,15,14) # "A witch! A witch! Burn her! Burn!" ```