Example of Natural Deduction for Colonel West“The law says that it is a crime for an American to sell weapons to a hostile nation. The country Nono, an enemy of America, has some missles, and all of its missles were sold to it by Colonel West, who is an American.” Prove Colonel West is a criminal.“The law says that it is a crime for an American to sell weapons to a hostile nation.”1. x,y,z american(x)  weapon(y)  nation(z)  hostile(z)  sells(x,y,z)  criminal(x)“The country Nono is an enemy of America.”2. nation(Nono)3. enemy(Nono,America)4. x nation(x)  hostile(x,America)  hostile(x)“The country Nono has some missles.”5. x missle(x)  owns(Nono,x)6. x missle(x)  weapon(x)“All of Non’s missles were sold to it by Colonel West.”7. x missle(x)  owns(Nono,x)  sells(West,x,Nono)“Colonel West is an American.”8. American(West)9. missle(m1)  owns(Nono,m1) [existential instantiation/skolemization of 5, ={x/m1}]10. missle(m1) [and elimination on 9]11. weapon(m1) [modus ponens on 6 an 10, ={x/m1}]12. hostile(Nono) [modus ponens on 2, 3, and 4, ={x/m1}]13. sells(West, m1,Nono) [modus ponens on 7 an 9, ={x/m1}]14. criminal(West) [modus ponens on 1, 8, 2, 12, 11, and 13, ={x/West,y/m1,z/Nono }]Example of Resolution Proof that Curiosity Killed the Cat“Everyone who loves all animals is loved by someone.”x [y animal(y)loves(x,y)] z loves(z,x)convert to CNF:x [y animal(y)  loves(x,y)]  z loves(z,x) - implication eliminationx y [animal(y)  loves(x,y)]  z loves(z,x) - push negations inwardx y [animal(y)  loves(x,y)]  z loves(z,x) - DeMorgan’s Lawx [animal(F(x))  loves(x,F(x))]  loves(G(x),x) - F(x) and G(x) are skolem functionsx [animal(F(x))  loves(G(x),x)]  [loves(x,F(x))  loves(G(x),x)] - distributivitythink of F(x) as a hypothetical animal not loved by x; by slight abuse of terminology, call it their “skolem”1. animal(F(x))  loves(G(x),x) - either x’s skolem is an animal, or someone G loves x2.  loves(x,F(x))  loves(G(x),x) - either x does not love their skolem, or someone G loves x“Anyone who kills an animal is loved by no one.”x [z animal(z)kills(x,z)]y loves(y,x)convert to CNF:x [z animal(z)kills(x,z)]  y loves(y,x)x z [animal(z)kills(x,z)]  y loves(y,x)x z animal(z)  kills(x,z)  y loves(y,x)3. animal(z)  kills(x,z)  loves(y,x)“Jack loves all animals.”x animal(x)  loves(Jack,x)4. animal(x)  loves(Jack,x)“Either Jack or Curiosity killed the cat, who is named Tuna.”5. kills(Jack,Tuna)  kills(Curiosity,Tuna)“Tuna is a cat and cats are animals.”6. cat(Tuna)x cat(x)  animal(x)7. cat(x)  animal(x)“Did Curiosity kill the cat?”negate the query to try to derive the empty clause by contradiction8. kills(Curiosity,Tuna)9. animal(Tuna) [reso on 6 and 7, ={x/Tuna}]10. loves(y,x)kills(x,Tuna) [reso on 3 and 9, ={z/Tuna}] - anyone who kills Tuna is loved by no one11. kills(Jack,Tuna) [ reso on 5 and 8]12. loves(y,Jack) [ reso on 10 and 11, ={x/Jack}] - no one loves Jack ( by contradiction)13.  animal(F(Jack))  loves(G(Jack),Jack) [reso on 2 and 4, ={x2/Jack,x4/F(Jack)}] - standardize variables apart14. loves(G(Jack),Jack)  loves(G(Jack),Jack) [reso on 13 and 1, ={x/F(Jack)}] - someone loves Jack15. loves(G(Jack),Jack) - collapse 2 identical terms to 116.  [reso on 12 and 14,