[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Current TLA Proof Rules

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
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.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2e13cc96-4e60-4264-bab8-b1b49a5a3178%40googlegroups.com.