Exercise 7.2

Re-prove the valid formula whose proof in the Hilbert calculus we have studied in Section 7.1.4 in our tableaux calculus. Think about the difference between positive and negative calculi.

Exercise 7.3

[You have to read the sidetrack on derived inference rules to do this exercise.] To see the value of the derived inference rules, prove or refute the formula .

Exercise 7.4

In Section 7.2.6 we claim that the utterance ``Mary doesn't like Mutz'' is inconsistent with the discourse ``If Mutz is a Siamese cat, then Mary likes her. Mutz is a Siamese cat.'' because we can construct a closed tableaux for the formula:

resp. the equivalent:

Construct this tableaux.

Then construct the tableaux needed to check whether ``Mary has a husband.'' is informative in the context ``If Mary is married then she has a husband. She is married.'' (treating the pronouns as in the example above).

For both examples, you may either use the derived inference rules from Section 7.2.8, or start of with a formula that uses only and .