Propositional Dynamic Logic (SNF)

This version of PDL first transforms formulae into a *-normal form defined in the associated paper. The conversion to *-normal form can result in a blow up of the given formula e.g. < * * a > p gets converted to < (a ; *a) ; * (a ; *a) > p. Since this is suboptimal, there is another prover that does not require *-normal form. The rules of that prover are currently being written up. 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. For an introduction to PDL see http://plato.stanford.edu/entries/logic-dynamic/
Results
Query
'''Syntax''' _ ::= blank AFml ::= a | b | c | ... APrg ::= p | q | r | ... Prg π ::= APrg | π ; π | π U π | _?_φ | _* π Fml φ ::= AFml | Verum | Falsum | ~_φ | φ v φ | <π> φ | φ -> φ | < π > φ | [ π ] φ ''Notes:'' (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.
Info
pdlMark.ml : Download
pdlMarkFunctions.ml : Download
pdlMarkRewrite.ml : Download