(Based on “The Adventure of Silver Blaze,” an original Sherlock Holmes mystery by Arthur Conan Doyle)

A prize-winning racehorse named Silver Blaze has been stolen from a stable, and a bookmaker named Fitzroy Simpson has been arrested as the prime suspect by good old Inspector Gregory. Sherlock Holmes, however, after ample use of his magnifying glass and some of the strongest black tobacco this side of the Atlantic, finds the true thief by reasoning from the following premises:

• The horse was stolen either by Fitzroy or by its trainer John Straker.
• The thief had to have entered the stable the night of the theft.
• If a stranger enters the stable, the dog barks.
• Fitzroy was a stranger.
• The dog did not bark.

Who stole Silver Blaze?

1. Encode all the given information as a knowledge base in propositional logic.
2. Write down which propositional symbols you used and which facts in the environment they represent.
3. Use the inference rules and equivalences below to infer who is the thief. For each inference step note which sentences and which inference rule / equivalence you used!

• Each propositional symbol stands for a statement about the environment that is either true or false. So “Fitzroy” is not a useful symbol, because it is a person but not something that is true or false. However, “Fitzroy_is_the_Thief” would be a useful symbol, although you should probably shorten it so you don't have to write so much.
• You should have 7 symbols in total, but different solutions are possible.
• When doing the inference do not think about the meaning of the symbols or which things are true and which are false! Just mechanically match the patterns of the inference rules with the sentences in your knowledge base to generate new sentences.
• Equivalences can be used as inference rules in both directions. E.g., <latex>$ \alpha \Rightarrow \beta \: \equiv \: \neg \alpha \lor \beta $</latex> means <latex>$\{ \alpha \Rightarrow \beta, . \} \: \vdash \: \neg \alpha \lor \beta $</latex> and <latex>$\{ \neg \alpha \lor \beta, . \} \: \vdash \: \alpha \Rightarrow \beta $</latex>
• You can the latex template on MySchool for your answers. If you do not have Latex installed, you can use https://www.writelatex.com/ to edit a Latex file and generate the pdf for submission.

1. <latex>$\{ \alpha \Rightarrow \beta, \alpha \} \: \vdash \: \beta $</latex>
2. <latex>$\{ \alpha \Rightarrow \beta, \neg \beta \} \: \vdash \: \neg \alpha $</latex>
3. <latex>$\{ \alpha \land \beta \} \: \vdash \: \alpha $</latex>
4. <latex>$\{ \alpha , \beta \} \: \vdash \: \alpha \land \beta $</latex>
5. <latex>$\{ \alpha \} \: \vdash \: \alpha \lor \beta $</latex>
6. <latex>$\{ \alpha \lor \beta, \neg \alpha \} \: \vdash \: \beta $</latex>
7. <latex>$ \alpha \Leftrightarrow \beta \: \equiv \: \beta \Leftrightarrow \alpha $</latex>
8. <latex>$ \alpha \Leftrightarrow \beta \: \equiv \: (\alpha \Rightarrow \beta) \land \beta \Rightarrow \alpha $</latex>
9. <latex>$ \alpha \Rightarrow \beta \: \equiv \: \neg \alpha \lor \beta $</latex>
10. <latex>$ \alpha \land \beta \: \equiv \: \beta \land \alpha $</latex>
11. <latex>$ \alpha \lor \beta \: \equiv \: \beta \lor \alpha $</latex>
12. <latex>$ \neg (\alpha \land \beta) \: \equiv \: \neg \alpha \lor \neg \beta $</latex>
13. <latex>$ \neg (\alpha \lor \beta) \: \equiv \: \neg \alpha \land \neg \beta $</latex>
14. <latex>$ \neg \neg \alpha \: \equiv \: \alpha $</latex>