pdltableau
pdltableau is a experimental implementation of the tableau calculus for PDL in De Giacomo and Massacci (2000), "Combining Deduction and Model Checking into Tableaux and Algorithms for ConversePDL" (Information and Computation 162, pp. 117137). An earlier version of this system is due to Renate A. Schmidt.
pdltableau is written in Prolog and should work with all recent versions of SWIProlog and other ISOcompliant Prolog systems. The source code for pdltableau is available here (Version 1.1).
Changes: 1.1
 Bug fixes related to detecting unfulfilled eventualities. See formulae 105 to 107 in problems.pl for examples which weren't handled correctly by pdltableau Version 1.0. The examples are due to Florian Widmann. Caching and reuse of `consistent sets' has been disabled.
 1.0
 Initial release
The formula input language
Atoms
Names for propositional atoms and atomic action symbols must be strings with lowercase first letters.Formulae
 The primitive connnectives are:

true, false, not(Fml), and(Fml1,Fml2), or(Fml1,Fml2), dia(Act,Fml), box(Act,Fml)
 Defined connnectives are:

implies(Fml1,Fml2), implied(Fml1,Fml2), equiv(Fml1,Fml2)
Actions
 The primitive action connnectives are:

true, or(Act1,Act2), comp(Act1,Act2), star(Act), test(Fml)
 Defined action connnectives are:

plus(Act)
Theory formulae
 A possibly empty list of formulae inside a pair of '[', ']' (the brackets are important).

[] [ Fml1, ..., Fmln ]
What does the prover do?
 The prover tests for satisfiability and interprets the input likes this:

and( forall([x], TheoryFml1(x)), ..., forall([x], TheoryFmln(x)), exists([x], InputFml(x)) )
The output
The output is the derivation given by a list of the inference steps performed. Each line has 3 items: the number of the inference step, a formula and a justification for the formula. An unnumbered line is a conclusion which is redundant. The items marked with `post' are the results of ignorability tests.