pdl-tableau

pdl-tableau 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 Converse-PDL" (Information and Computation 162, pp. 117-137).

Web-interface

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.
pdl-tableau
Home | Web Interactive Input Form

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 15 Feb 12
Copyright © 2003-2004 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk