--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9811f409-94b8-42d4-b56b-2ff4b2739886n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8bd4439d-7f5d-4e5d-b935-7c4d8b71b4ban%40googlegroups.com.
The proof on pages 24-25 of the corollary stated on the preceding page was checked by TLAPS.
From:
tla...@googlegroups.com <tla...@googlegroups.com> On Behalf Of
marta zhango
Sent: Thursday, April 25, 2024 9:35
To: tlaplus <tla...@googlegroups.com>
Subject: Re: [tlaplus] TLA and TLAPIS
You don't often get email from marta...@gmail.com. Learn why this is important |
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bdc5219c-0411-4355-91f6-af1ee5f218a3n%40googlegroups.com.
On 25 Apr 2024, at 18:34, marta zhango <marta...@gmail.com> wrote:
I am getting very confused. About (1) an easy outline of a proof and (2) the complete code for a proof system to check it.
The complete code for checking a proof can be enormously complicated, especially when one has to declare a significantnumber of functions and constructs.Consider "Appendix A: Formal Proof" ( https://lamport.azurewebsites.net/pubs/proof.pdf ) containing a TLA+ formalizationof Spivak’s proof. That is not the actual complete code for a proof system to check it, am I right ?
Now, about comment regarding the proof in Cantor10.tla. Is that the actual complete code for a proof system to check thecorrectness of the proof ? Or is it a description of the proof.
I want to write some proofs from signal processing that are more formal than the standard way of showing a proof in atextbook, but not as complicated as the complete code required by a proof system. What would you suggest ?
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bdc5219c-0411-4355-91f6-af1ee5f218a3n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/95b0937e-361c-4d29-99e6-60f5924d3ee7n%40googlegroups.com.