pdl-tableau 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 Converse-PDL" (Information and Computation 162, pp. 117-137). An earlier version of this system is due to Renate A. Schmidt.

pdl-tableau is written in Prolog and should work with all recent versions of SWI-Prolog and other ISO-compliant Prolog systems. The source code for pdl-tableau is available here (Version 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 pdl-tableau Version 1.0. The examples are due to Florian Widmann. Caching and re-use of `consistent sets' has been disabled.
Initial release

The formula input language


Names for propositional atoms and atomic action symbols must be strings with lowercase first letters.


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)


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

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:
        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.


We look forward to your feedback. Please send your comments and suggestions to u.hustadt@liverpool.ac.uk.