Exercise 8.1

Implement the derived inference rules from Section 7.2.8 using the ideas in this chapter. Include in your solution the examples that you used to test your implementation.

Exercise 8.2

Draw a tableaux for, and run the implemenation with the input:

If you expand the first conjunct first (as our implementation does), the second conjunct will have to be expanded on two branches.

Make sure you understand how this is done in our implementation. You can either perform a trace or draw a computation tree.

Exercise 8.3

In Section 7.2.1 we used little check marks () to signify that a formula had been expanded. In Section 7.2.3, we said that we do not expand formulae twice in order to ensured termination of the tableaux construction process. Now there's no obvious equivalent to such a technique in our implemenation. It terminates although it does not keep any explicit record of which formulae have already been expanded. Why doesn't it keep on expanding the same formulae for ever? In other words: How does our program know when a tableaux is saturated?