The prover PDL SNF 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 PDL No SNF that does not require *-normal form. The rules of the prover PDL No SNF are currently being written up.

Click on a pre-written formula:

[p] (a -> b) -> ([p] a -> [p] b)
[p] (a & b) <-> ([p]a & [p]b)
[p U q]a <-> ([p] a & [q] a)
[p;q]a <-> [p] [q] a
a & [p] [*p] a <-> [*p] a
a & [*p]( a -> [p]a) -> [*p] a
[*p](a -> [p]a) -> (a -> [*p]a)
~ ( < b ; * a > p & [ * b ; * a ] ~ p )
< *a> p <-> p v <a> < *a> p
[*p]a -> [p]a
[*(p U q)]a -> [p U q]a
[*p]a -> [*p][*p] a
[p][*q]a -> [p U(p;q)]a
[*(p U q)]a -> [*p][*q]a
[*p]a -> [*(p;p)]a
[p;*(q;p)]a -> [*(p;q);p]a
[? b]a <-> (b -> a)
~(< *( *p U *q) >a & [*p]~ a & [ *q]~ a)
[ * * * * * * * * * * * * * p] Verum
~ (< ? (~ ~ ~ a)>a)
Syntax: 

 _ ::= blank 
 AFml ::= a | b | c | ... 
 APrg ::= p | q | r | ... 
 Prg π ::= APrg | π ; π | π U π | _?_φ | _* π 
 Fml φ ::= AFml | Verum | Falsum | ~_φ | φ v φ | φ Λ φ 
    | φ -> φ | < π > φ | [ π ] φ
Notes:
SNF is a Star-Normal-Form defined in our paper
Star (*) is a prefix operator rather than a postfix one so *a is okay but a* is not.
Star (*) and test (?) require a space before them.
Negation ~ requires a space after it so ~ ~ p0 is okay but ~~p0 is not okay.
Important: if you use incorrect syntax then the prover will not complain, it will just not return a result.


Current Results:

Previous Results: