There are four people: Roberta, Thelma, Steve, and Pete.
Among them, they hold eight different jobs.
Each holds exactly two jobs.
The jobs are chef, guard, nurse, clerk, police officer (gender not implied), teacher, actor, and boxer.
The job of nurse is held by a male.
The husband of the chef is the clerk.
Roberta is not a boxer.
Pete has no education past the ninth grade.
Roberta, the chef, and the police officer went golfing together.
Question: Who holds which jobs?
Solution: This puzzle has been solved by intelligent middle-school children.
We present the puzzle here as an example of some of the challenges one faces in representing implicit as well as explicit information to an automated reasoning program.
A detailed discussion of this puzzle and others is given in Automated Reasoning: Introduction and Applications, by Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. The book, published by McGraw-Hill, includes a diskette of the automated reasoning program OTTER, which can be used to solve puzzles as well as extremely challenging problems in mathematics and logic.
Those who have OTTER already may simply take the input and start experimenting.