pdl-tableau
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).
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 pdl-tableau Version 1.0. The examples are due to Florian Widmann. Caching and re-use 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.