The Tableau WorkBench (TWB)

The rules of this prover and their proofs of soundness and completeness are given in a manuscript which can be found at http://arxiv.org/abs/0711.1016 via the world wide web. For an introduction to PDL see http://plato.stanford.edu/entries/logic-dynamic/ When you enter a formula A, then "closed" means that A is a theorem because the tableau for ~ A is closed, and "open" means that it is not a theorem because the tableau for ~ A is open.

Results

Query

Non Theorems: Select One< * * a > p< * * * a > p< * * * * a > p

Theorems: Select One[p] (a -> b) -> ([p] a -> [p] b)[p] (a & b) <-> ([p]a & [p]b)[p U q]a <-> ([p] a & [q] a)[p;q]a <-> [p] [q] aa & [p] [*p] a <-> [*p] aa & [*p]( a -> [p]a) ->[*p] a[*p](a -> [p]a) -> (a -> [*p]a)~ ( < b ; * a > p & [ * b ; * a ] ~ p )< *a> p <-> p v <a> < *a> p[*p]a -> [p]a[*(p U q)]a -> [p U q]a[*p]a -> [*p][*p] a[p][*q]a -> [p U(p;q)]a[*(p U q)]a -> [*p][*q]a[*p]a -> [*(p;p)]a[p;*(q;p)]a -> [*(p;q);p]a[ ? b ]a <-> (b -> a)

Input One:

'''Syntax'''
_ ::= blank

AFml ::= a | b | c | ...

APrg ::= p | q | r | ...

Prg π ::= APrg | π ; π | π U π | _?_φ | _* π

Fml φ ::= AFml | Verum | Falsum | ~_φ | φ  v φ | <π> φ | φ -> φ | < π > φ | [ π ] φ

''Notes:''

(1) Star (*) is a prefix operator rather than a postfix one so *a is okay but a* is not.

(2) Star (*) and test (?) require a space before them.

(3) Negation ~ requires a space after it so ~ ~ p0 is okay but ~~p0 is not okay.

Info

pdlMarkNoSnf.ml : Download
pdlMarkNoSnfFunctions.ml : Download