Linear Temporal Logic

Salomon Sickert with contributions from Benedikt Seidl

1 March 2016


This theory provides a formalisation of linear temporal logic (LTL) and unifies previous formalisations within the AFP. This entry establishes syntax and semantics for this logic and decouples it from existing entries, yielding a common environment for theories reasoning about LTL. Furthermore a parser written in SML and an executable simplifier are provided.
BSD License

Change history

[2019-03-12] Support for additional operators, implementation of common equivalence relations, definition of syntactic fragments of LTL and the minimal disjunctive normal form.

Depends On

Used by


Related Entries