Consider the following logic puzzle, which is one of many created by Lewis Carroll, the author of Alice in Wonderland.
No birds, except ostriches, are 9 feet high. There are no birds in this aviary that belong to anyone but me. No ostrich lives on mince pies. I have no birds less than 9 feet high.
Prove that these premises imply the following conclusion:
Any bird in this aviary does not live on mince pies.
Use the following symbols to represent statements:
H: Height of the bird is not less than nine feet. O: The bird is an ostrich. M: The bird lives on mince pies. I: I own the bird. A: The bird is in this aviary.
- Show the premises as logical formulas represented using these symbols. $$O \rightarrow H$$ $$A \rightarrow I$$ $$O \rightarrow \neg M$$ $$I \rightarrow H$$
- Show the conclusion as a logical formula represented using these symbols. $$A \rightarrow \neg M$$
- Show the negation of the conclusion using these symbols. $$\neg (A \rightarrow \neg M)$$
- Show all premises and the negation of the conclusion as a set of clauses. $$A \wedge M, \neg O \vee H, \neg A \vee I, \neg O \vee \neg M, \neg I \vee H$$
- Use the resolution method for your proof, and show for each resolution step which formulas are involved as parents and what the resolvent is. ???