This version of our prover is able to classify each branch as either closed or open at its leaf.

Thus there is no need for the variable UEV which was used to identify Unfulfulled EVentualities

and then was passed up from children to parents in our other tableau procedures PDL (UEV).

For an introduction to PDL see http://plato.stanford.edu/entries/logic-dynamic/

When you enter a formula A, then "closed" means that A is a

theorem because the tableau for ~ A is closed, and "open" means

that it is not a theorem because the tableau for ~ A is open.