The Tennis Lover

Stolen from an anonymous worksheet, posted on the web at University of California Irvine, which says that it comes from an advert for a tennis magazine.

Your problem is to use propositional logic to represent the following example of reasoning, and use the Prover9 theorem prover to prove that the reasoning is valid.

Use the following template file to create your Prover9 encoding of the problem: tennis.p9

Marks: There are two marks for each sentence, making a total of 8 marks.

Outline: This problem is a bit different from most of the others ones. Rather than being given a specific goal, you need to find an appropriate goal, which both answers the question and is provable from the assumptions. You should try possible goals one at a time, until you find one that is provable. Alternatively, you could work out the goal by your own reasoning and then check it using Prover9. Of course, if you have represented the other sentences incorrectly, the correct goal may not be provable, and possibly a different goal could be provable. So you may need to check and alter the other formulae to get a proof of the correct goal.

Problem Statement

A1	If I'm not playing tennis, I'm watching tennis.
A2	If I'm not watching tennis, I'm reading about tennis.
A3	I cannot do more than one tennis-related activity at the same time. *
Goal	What am I doing? **

Non-Logical Vocabulary

Propositional Constants: Playing, Watching, Reading

Notes:

* You need to find a propositional formula involving the 3 tennis activity propopositions which is true if only one or none of these is true
** Try each of the activies to find the one that can be proved to be true. Do not put several different goals in together. Although, Prover9 does allow multiple formulae in the goal section, this will not give the proof of a specific answer that we want.