Propositional Dynamic Logic PDL (No UEV)

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

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.


_ ::= blank

AFml ::= a | b | c | ...

APrg ::= p | q | r | ...

Prg π ::= APrg | π ; π | π U π | _?_φ | _* π

Fml φ ::= AFml | Verum | Falsum | ~_φ | φ v φ | <π> φ | φ -> φ | < π > φ | [ π ] φ


(1) Star (*) is a prefix operator rather than a postfix one so *a is okay but a* is not.

(2) Star (*) and test (?) require a space before them.

(3) Negation ~ requires a space after it so ~ ~ p0 is okay but ~~p0 is not okay.