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