Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Linear Temporal Logic


view this post on Zulip Email Gateway (Aug 22 2022 at 12:53):

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: Apr 20 2024 at 12:26 UTC