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