Linear Temporal Logic

Salomon Sickert 🌐 with contributions from Benedikt Seidl 📧

March 1, 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


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


Session LTL