As regards the first task, our decision is this: We do not represent tableaux explicitely. Rather, we use Prolog's backtracking mechanism to "crawl along" the tableaux under construction. This makes the second task almost trivial - really all we have to do is translate our inference rules into Prolog. The resulting program is somewhat different from what you might expect if you think about constructing tableaux with pen and paper. Nevertheless it's elegant and easily implemented.
Implement the derived inference rules from » Sidetrack: Practical Enhancements for Tableaux using the ideas in this chapter. Include in your solution the examples that you used to test your implementation.
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.
In » Tableaux for Theorem Proving we used little check marks (✓) to signify that a formula had been expanded. In » Analytical Tableaux: A more formal Account, 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?