(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?

Prove your assertion using the technique of resolution. Construct your resolution proof using only the following proposition symbols:

• ThiefFitzroy
• ThiefJohn
• EnteredStableFitzroy
• EnteredStableJohn
• StrangerFitzroy
• StrangerJohn
• BarksDog

Tasks:

1. Encode all the given information as a knowledge base KB in propositional logic using the given propositional symbols.
2. Guess an answer and formulate it as a sentence A in propositional logic.
3. Proof that your guess is right (KB entails A) using resolution.

Encode the information for the problem above in First-Order Logic (FOL):

1. Decide which constants, functions, and predicates you want to use.
2. Write down FOL sentences for the given facts.
3. Compare the size of the FOL knowledge base with the size of the propositional knowledge base.