Linear Temporal Logic

Salomon Sickert 🌐 with contributions from Benedikt Seidl 📧

March 1, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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