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

*From*: marta zhango <martazhango@xxxxxxxxx>*Date*: Thu, 25 Apr 2024 07:58:36 -0700 (PDT)*References*: <9811f409-94b8-42d4-b56b-2ff4b2739886n@googlegroups.com> <7D444807-747B-40F6-9AD9-EB3A203EADA3@gmail.com>

For instance, consider the TLA+2 Proof of Cantor’s Theorem ( see first theorem of appendix B in

https://lamport.azurewebsites.net/pubs/keappa08-web.pdf ) as a proof in a mathematics textbook.

That would be more suitable than a TLAPS version of it. TLAPS is a translation of a TLA+2 Proof

for checking the proof. In such a description correct ?

As you say, a detailed proof written in a way that enables it to be checked by an automated system

requires substantial effortfrom the user.

For a textbook, an outline of the proof using TLA+2 could be the formal proof. Which can then be

checked out by coding the corresponding instructions for a proof checker.

On Friday, April 26, 2024 at 2:20:42 AM UTC+12 Stephan Merz wrote:

Could you elaborate on what you mean by referring to TLA as a way to outline a proof? TLA stands for Temporal Logic of Actions, so it is a logic rather than a proof system – although the TLA paper [1] includes proof rules that can be (mainly) used in paper-and-pencil proofs.Like Coq and Lean, TLAPS is a mechanical proof assistant that allows you to write a detailed proof and have it checked by the system. These tools indeed require substantial effort from the user, but unlike model checkers such as TLC they can (in principle) verify correctness properties for arbitrary specifications, not only finite-state systems.StephanOn 25 Apr 2024, at 14:38, marta zhango <marta...@xxxxxxxxx> wrote:There seems to exist a big difference between TLA and TLAPIS. TLA is a way to outline a proof, whilst TLAPIS, Coq, Lean provide ways to check whether a proof is correct. With theproof checkers being quite long and time consuming to construct.In this correct ?--

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9811f409-94b8-42d4-b56b-2ff4b2739886n%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/8bd4439d-7f5d-4e5d-b935-7c4d8b71b4ban%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] TLA and TLAPIS***From:*Stephan Merz

**References**:**[tlaplus] TLA and TLAPIS***From:*marta zhango

**Re: [tlaplus] TLA and TLAPIS***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLA and TLAPIS** - Next by Date:
**Re: [tlaplus] TLA and TLAPIS** - Previous by thread:
**Re: [tlaplus] TLA and TLAPIS** - Next by thread:
**Re: [tlaplus] TLA and TLAPIS** - Index(es):