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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 15 Oct 2019 08:58:47 +0200*References*: <2e13cc96-4e60-4264-bab8-b1b49a5a3178@googlegroups.com>

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

**References**:**[tlaplus] Current TLA Proof Rules***From:*JosEdu Solsona

- Prev by Date:
**Re: [tlaplus] Beginner Question: Working with the Prisoners Example** - Next by Date:
**Re: [tlaplus] Beginner Question: Working with the Prisoners Example** - Previous by thread:
**[tlaplus] Current TLA Proof Rules** - Next by thread:
**[tlaplus] State graph of distinct states** - Index(es):