'''NB''': We are working to make the implementation of this calculus available on this website by the end of the week.
'''UPDATE''':
* pdlMarkedNoSnf.ml : http://twb.rsise.anu.edu.au/propositional_dynamic_logic_no_snf
* pdlMarked.ml: http://twb.rsise.anu.edu.au/propositional_dynamic_logic_snf
alternatively you can also check this out : http://users.rsise.anu.edu.au/~rpg/pdlweb/
paper accepted to m4m http://m4m.loria.fr/M4M5/
==Abstract==
We present a tableau-based algorithm for deciding satisfiability for
propositional dynamic logic (PDL) which builds a finite rooted tree
with ancestor cycles and which passes extra information from
children to parents to separate good cycles from bad cycles during
backtracking. It is easy to implement, with potential for
parallelisation, because it constructs a potential model ``on the
fly'' by exploring each tableau branch independently. However, its
worst-case behaviour is 2EXPTIME rather than EXPTIME. We give
detailed proofs of soundness and completeness in an appendix and
there is a prototype implementation in the TWB.
We implemented two provers (that will be shortly in the website demo section):
===pdlMarked.ml: ===
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.
===pdlMarkedNoSnf.ml: ===
This version of PDL uses just negation normal form and does not
require a *-normal form. The rules of this prover are more
complicated and their proofs are currently being written up.