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

• Web-interface

Usage

Just type in a formula and some theory formulae, and press the Submit button.

Warning

The formula input language

Atoms

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