Re: [tlaplus] Current TLA Proof Rules

Hello,

I think that Leslie's TLA paper (1994) is the standard reference for TLA proof rules. My paper from 2003 does not claim to present a complete proof system, and the Hyperbook is more of a tutorial introduction to the use of TLA+ for modeling and verifying systems.

The differences between the rules that you mention are in fact minor, although it is admittedly unfortunate that the same name is used for different rules, and indeed the rule called (TLA2) in my 2003 paper is closer to (INV2) from (Lamport, 1994) in a different clothing.

I believe that the use of double bars in the Hyperbook is meant as a reminder that proof rules in modal / temporal logics are substantially different from those in predicate logic, and in particular that one cannot identify a sequent A |- B with the validity of the implication A => B. Although the correct interpretation of TLA proof rules is given in a footnote in (Lamport, 1994), a clearer visual indication of this difference is probably useful.

TLAPS does not allow the user to write temporal proof rules. It is meant to help proving properties of systems, i.e. implications of the form Spec => Property. The necessary rules for temporal reasoning are built into the PTL decision procedure, and there will eventually be another backend for first-order temporal reasoning, such as the LATTICE rule. We have so far deliberately avoided adding syntax for temporal proof rules in order to avoid the extra mental burden that these incur. Experience will show if we need to add such syntax for more complex temporal reasoning.

Best regards,

Stephan

On 6 Oct 2019, at 19:33, JosEdu Solsona <josedusolsona@xxxxxxxxx> wrote:

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.

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

--
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/494F5A18-2065-4926-97F9-3256D93EE72A%40gmail.com.