pdltableau
pdltableau is a prototypical implementation of a variation 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).
Webinterface
Usage
Just type in a formula and some theory formulae, and press the Submit button.
Warning
At the moment there is no guarantee for the soundness of the procedure
for formulae containing nested occurrences of the star operator.
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.
Feedback
We look forward to your feedback. Please send your comments and suggestions
to
schmidt@cs.man.ac.uk.
pdltableau
Home 
Web Interactive Input Form
Renate A. Schmidt
Home 
Publications 
Tools 
FM Group 
School 
Man Univ
Last modified: 15 Feb 12
Copyright © 20032004
Renate A. Schmidt,
School of Computer Science, Man Univ, schmidt@cs.man.ac.uk