From: Tobias Nipkow <nipkow@in.tum.de>
Linear Temporal Logic
Salomon Sickert
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.
http://afp.sourceforge.net/entries/LTL.shtml
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC