This Web page describes my encoding of Lamport's
Temporal Logic of Actions
in the higher-order logic of the generic interactive proof assistant
TLA has been included with the standard distribution of Isabelle.
To avoid versioning problems, it is therefore no longer available
for separate download.
Isabelle/TLA is based on a complete axiomatization of the "raw"
(stuttering-sensitive) variant of TLA. Here are two notes on the
design of the
prover and on a completeness proof
for the underlying axiom system.
You may also browse the
for the various theories.
The distribution contains a few examples, including
Please let me know about any comments or suggestions.