The Tableau WorkBench (TWB)

Also known as Weak S5 (WS5) because it lacks reflexivity, this logic is often used as the basis of logics of agents where []p means "the agent knows p" or "the agent believes p".

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 A is not a theorem because the tableau for ~ A is open.

Prover for modal logic KD45.
Based on:
Efficient Loop-Check for KD45 Logic
A Birstunas
Lithuanian Mathematics Journal 46(1):44-53 2006.

Author: Rajeev Gore 01 November 2007 (Copyright).

Results

Query

Non Theorems: Select Onep -> []<>p[]p -> p<>[]p -> p

Theorems: Select One[] (a -> b) -> ([] a -> [] b)[]p -> <>p[]p -> [][]p<>[]p -> []p<>[]p -> []<>[]p<>([]p -> p)[](p -> []<>p)[][]p -> []p(<>p & <>q) -> <>(p & <>q)

Input One:

ATOM := a | b | c | ...
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| [] formula
| <> formula
| ~ formula

Info

kd45Birstunas.ml : Download

KD extends basic normal modal logic K with the axiom
D = []p -> <>p which forces the binary Kripke relation to be serial or total.
That is, for every world w, there is a world v such that w R v holds.

KD is characterised by finite rooted trees where only the leaves have to be reflexive
since all internal nodes have an R-successor.

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[] p[] p1 -> [] [] p1~ [] p1 -> [] ~ [] p1[] Falsum

Theorems: Select One[]p -> <> p<> Verum<> p -> <> p<> p -> [] ( [] ~ q v <> q)~ ( <> p & [] ~ p )~ ( <> p & <> ( <> q & ~ <> q) )[] (a -> b) -> ([] a -> [] b)[] (p0 & p1) <-> ([] p0 & [] p1) )<> (p0 v p1) <-> (<> p0 v <> p1) )~ [] ~ p0 <-> <> p0 )( [](p0 -> p1) -> ([] p0 -> [] p1) )~ [] (p & ~ p)

Input One:

ATOM := a | b | c | ...
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| [] formula
| <> formula
| ~ formula

Info

kd.ml : Download

Propositional Linear Temporal Logic, also known as Propositional Linear Time Logic has the natural number
line ordered by < as the intended model. It is used to model temporal behaviour with two basic modal
operators X p interpreted as "the next state makes p true" and p Un q interpreted as "p is true from now
until q becomes true". The other operators are defined from these.

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( X p1 -> p1 )( F p1 -> X p1 )( X p1 -> X X p1 )( G (p1 v p2) <-> G p1 v G p2 )( (F (p1 & p2)) <-> (F p1 & F p2) )( ((p0 Un p2) v (p1 Un p2)) <-> ((p0 v p1) Un p2) )(G F p0 & G F p1) & G (p0 -> (~ p1 & X ~ p1)) & G ( p1 -> (~ p0 & X ~ p0)) & (~ p0 & ~ p1)G F (p0 & (p1 Un ~ p0)) & G F (p0 & (~ p1 Un ~ p0))p0 & G(p1 -> ~ p0) & X p1 & X F p0

Theorems: Select One(G (a -> b)) -> (G a -> G b)(X (a -> b)) -> (X a -> X b)(X ~ a) <-> ~ X a(G a) -> (a & X G a)G(a -> X a) -> (a -> G a)(a Un b) -> (F b)(a Un b) <-> (b v (a & X (a Un b)))((X ~ p0) <-> ( ~ X p0 ) )((~ G ~ p1) <-> F p1 )(( p0 & G (p0 -> X p0)) -> G p0 )(G(p1 & p2) <-> ((G p1) & (G p2)) )(G p1 ) -> ( G G p1 )( X G p0 ) <-> ( G X p0 )( ( G (p1 -> p2) ) -> ((G p1) -> G p2) )( (p0 Un p1) <-> (p1 v ( p0 & X ( p0 Un p1)) ))( (p0 Un p1) <-> ~ ( ~ p0 Bf p1) )( (p0 Un p1) -> F p1 )( (F p0) <-> (Verum Un p0) )( F(p1 v p2) <-> ( F p1 v F p2 ) )( ( F p0 ) <-> ( p0 v X F p0 ) )(G(p0 Un p1) & G(p0 -> p2) & G(p1 -> p2)) -> G p2

Input One:

ATOM := a | b | c | ...
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| formula U formula
| formula U formula
| X formula
| F formula
| G formula
| ~ formula

Info

Often known as Branching Time Temporal Logic, CTL allows us to state properties which may be true
on all paths or on some paths in a rooted tree where each branch is a copy of the natural numbers.

For an introduction to temporal logics, see
http://plato.stanford.edu/entries/logic-temporal/

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.

When you enter a formula A, then "closed" means that A is a

Results

Query

Non Theorems: Select One~ ( AG (AF (p & q) & AF (p & ~ q) & AF (~ p & q)) )AG ((p v AG q) & ( AG p v q )) <-> (AG p v AG q)~ (EG (( (AX (EF p1)) & (~ p1)) ))

Theorems: Select One(E p U q) -> (E p U q)(E p U q) -> EF q(A p U q) -> (A p U q)(A p U q) -> AF qAF a <-> (A Verum U a)EF a <-> (E Verum U a)AG a <-> ~ ( E Verum U ~ a)EG a <-> ~ ( A Verum U ~ a)A p U q <-> q v (p & AX (A p U q))E p U q <-> q v (p & EX (E p U q))~ ( AG p & EF ~ p )AG (p -> q) -> ( AG p -> AG q)AX (p -> q) -> ( AX p -> AX q)(AG p) -> (AX p & AX AX AG p)(AG (p -> AX p)) -> (p -> AG p)(AG (p -> q)) -> (EG p -> EG q)EG p -> ( p & EX EG p )AG p -> EG p(AG ( p -> EX p)) -> (p -> EG p)AG p -> pAG p -> AF pAX (p -> q) -> ( EX p -> EX q)AG (p -> q) -> ( AF p -> AF q)EG p -> EX pAX p -> EX p(AG (p & q)) <-> (AG p & AG q)(EG (p & q)) -> (EG p & EG q)(AX (p & q)) <-> (AX p & AX q)(EX (p & q)) -> (EX p & EX q)(AX p & EX q) -> EX (p & q)(AG p & EG q) -> EG (p & q)AG p <-> (p & AX AG p)EG p <-> (p & EX EG p)AG p <-> AG AG pEG p <-> EG EG p(EG (p -> AX p)) -> (p -> EG p)(AF AG p) -> AG AF pEG ((p v EG q) & ( EG p v q )) <-> (EG p v EG q)(AX AG p) <-> AG AX pEX EG p -> EG EX p

Input One:

ATOM := a | b | c | ...
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| E formula U formula
| A formula U formula
| EX formula
| AX formula
| AF formula
| EF formula
| AG formula
| EG formula
| ~ formula

Info

This version of our prover is able to classify each branch as either closed or open at its leaf.
Thus there is no need for the variable UEV which was used to identify Unfulfulled EVentualities
and then was passed up from children to parents in our other tableau procedures PDL (UEV).

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

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

This is a prover for KLM ( Kraus, Lehmann and Magidor ) logic P as defined in:
L Gordano, V Gliozzi, N Olivetti, G Pozzato
"Analytic tableaux for KLM Preferential and Cummulative Logic"
Proceedings of LPAR 2005 LNAI 3835:666-681, Springer, 2005.

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

Theorems: Select One(a => c) -> ( (a & c) => c )a => a(a => b) -> (a => b)((a => b) & (a => c)) -> ((a & b) => c)((a => b) & (a => c)) -> (a => (b & c))((a => c) & (b => c)) -> ((a v b) => c)

Input One:

Info

K4 has the following axion on top of normal modal logic K:
[]p -> [][]p which enforces that the Kripke reachability relation R is transitive.

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

Theorems: Select One[](p -> q) -> ([]p -> []q)[]p -> [][]p<> <>p -> <>p

Input One:

Info

Also known as KT4 this logic add the following axioms to K:
T = []p -> p which forces the Kripke reachability relation to be reflexive
4 = []p -> [][]p which forces the Kripke reachability relation to be transitive.

It is characterised by finite rooted transitive trees of clusters where a cluster
is a finite set of points with every world in the cluster reachable from every other world in the cluster.

When you enter a formula A, then "closed" means that A is a
theorem because the tableau for ~ A is closed, and "open" means

Results

Query

Non Theorems: Select Onep -> []<>p<>[]p -> []p[] ( p -> q) -> [] (q -> p)

Theorems: Select One[] a -> [] [] a[] <> a -> [] [] <> a[]((p -> q) <-> (~ q -> ~ p))[](~ (~ p) <-> p)[](~ (p -> q) -> (q -> p))[]((~ p -> q) <-> (~ q -> p))[](((p v q) -> (p v r)) -> (p v (q -> r)))[](p v ~ p)[](p v ~ (~ (~ p)))[](((p -> q) -> p) -> p)[]((((p v q) & (~ p v q)) & (p v ~ q)) -> ~ (~ p v ~ q))~ <>( ~ (p <-> q) & (q -> r) & (r -> (p & q)) & (p -> (q v r)) )[](p <-> p)[](((p <-> q) <-> r) <-> (p <-> (q <-> r)))[]((p v (q & r)) <-> ((p v q) & (p v r)))[]((p <-> q) <-> ((q v ~ p) & (~ q v p)))[]((p -> q) <-> (~ p v q))[]((p -> q) v (q -> p))[](((p & (q -> r)) -> s) <-> (((~ p v q) v s) & ((~ p v ~ r) v s)))([](p -> q) -> ([] p -> [] q))(([]([](p -> [] p) -> p) -> p) -> ([]([](p -> [] p) -> p) -> (<> [] p -> p)))(([]([](p -> [] p) -> p) -> [] p) -> ([]([](p -> [] p) -> p) -> (<> [] p -> [] p)))( []([] p -> [] [] p) & ([]([] p -> p) -> (<> [] p -> [] p)) -> ([]([](p -> [] p) -> p) -> (<> [] p -> [] p)) )( ([] p -> p) & ([]([](p -> [] p) -> p) -> (<> [] p -> [] p)) -> ([]([](p -> [] p) -> p) -> (<> [] p -> p)) )( []([] p -> p) & ([]([](p -> [] p) -> p) -> (<> [] p -> p)) -> ([]([](p -> [] p) -> p) -> (<> [] p -> p)) )( ([]([](p -> [] p) -> p) -> p) -> ([] p -> p) )([] p -> [] [] p)( []([] p -> [] q) -> [] []([] p -> [] q) )( []((<> [] p -> p) ) -> [] []((<> [] p -> p) ))( []([] p -> [] [] p) -> [] [] ([] p -> [] [] p) )([] p -> p)(p -> <> p)( []( []([](p -> [] p) -> p) -> (<> [] p) ) -> [] []( []([](p -> [] p) -> p) -> (<> [] p) )

Input One:

ATOM := a | b | c | ...
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| [] formula
| <> formula
| ~ formula

Info

s4.ml : Download

The basic normal modal logic K is characterised by the set of all Kripke frames with a binary reachability
relation. Its decision problem is PSPACE complete.

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[] p1 -> p1[] p1 -> [] [] p1~ [] p1 -> [] ~ [] p1

Theorems: Select One<> p -> <> p<> p -> [] ( [] ~ q v <> q)~ ( <> p & [] ~ p )~ ( <> p & <> ( <> q & ~ <> q) )[] (a -> b) -> ([] a -> [] b)( [](p0 & p1) <-> ([] p0 & [] p1) )( <>(p0 v p1) <-> (<> p0 v <> p1) )( ~ [] ~ p0 <-> <> p0 )( [](p0 -> p1) -> ([] p0 -> [] p1) )([] p0 -> <> p0) & ([] p0 -> [] [] p0) & (~ p0 -> [] <> ~ p0) -> ([] p0 -> p0)[] (<> ~ p0 v p0) v <> [] Falsum v <> ([] p0 & <> <> ~ p0) v <> ([] <> p0 & <> <> [] ~ p0) v <> (p0 & <> [] ~ p0) v <> (~ p0 & <> [] p0)

Input One:

formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| [] formula
| <> formula
| ~ formula

Info

k.ml : Download
klib.ml : Download

This version of PDL first transforms formulae into a *-normal form defined in the associated paper. The conversion to *-normal form can result in a blow up of the given formula e.g. < * * a > p gets converted to < (a ; *a) ; * (a ; *a) > p. Since this is suboptimal, there is another prover that does not require *-normal form. The rules of that prover are currently being written up. 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

pdlMark.ml : Download
pdlMarkFunctions.ml : Download
pdlMarkRewrite.ml : Download