Tableau

Propositional Modal Logic KD45

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

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

Info
kd45Birstunas.ml : Download

Propositional Modal Logic KD

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

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 PLTL

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

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

Propositional Computational Tree Logic CTL

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

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

Propositional Dynamic Logic PDL (No UEV)

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

'''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

Propositional KLM Logic P

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
Info

Propositional Modal Logic K4

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
Info

Propositional Modal Logic S4

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

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

Info
s4.ml : Download

Propositional Modal Logic K

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

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

Info
k.ml : Download
klib.ml : Download

Propositional Dynamic Logic (SNF)

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
'''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
Syndicate content