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