The rules of this prover and their proofs of soundness and completeness are given
in a manuscript which can be found at
http://arxiv.org/abs/0711.1016 via the world wide web.
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.