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
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
| E formula U formula
| A formula U formula
| EX formula
| AX formula
| AF formula
| EF formula
| AG formula
| EG formula
| ~ formula

Info