Hello all,
Since i'm interested in proofs, some time ago i started reading The Temporal Logic of Actions (Lamport, 1994), where there is a comprehensive presentation of the axioms and proof rules of TLA with justification and some introductory examples using the rules.
But, more recently, i'm also reading other sources like the Hyperbook (supposedly more up to date) and On the Logic of TLA+ (Merz, 2003). I have found some (minor?) differences between the presentations, for example
- TLA2 rule in Merz is like a specialized version of TLA2 original rule in Lamport.
- The Hyperbook doesn't mention the TLA1 and TLA2 original rules, but there is the INV2 rule which is the same as TLA2 rule in Merz.
- The LATTICE rule is now the leads-to induction rule, this is explained in the Hyperbook. Altough doesn't look the same i expect it to be equivalent.
- The Hyperbook differentiates ordinary proof rules from temporal proof rules using one bar or two bars. This distinction is not done anywhere else.
I understand TLA+ has evolved, and TLAPS is new in compassion to the original presentation.
Should i keep reading the Hyperbook as the official reference and not bother with old papers? (i mean, where possible, because the Hyperbook is not complete, and old papers have nice examples)
There is something like a current "standard" set of rules/axioms as in the original presentation?.
Any advice on what is the best path to follow for doing formal proofs will be appreciated.
Thanks.