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

*From*: marta zhango <martazhango@xxxxxxxxx>*Date*: Sun, 28 Apr 2024 00:42:07 -0700 (PDT)*References*: <48640047-49ce-4d12-899b-acea04612b3bn@googlegroups.com> <79520297-12e7-4df4-99d0-51e6b1a1dc40@gmail.com>

Felicitations Martin. The problem I struggle with is that the TLA+ book does not cover

the verification of mathematical proofs. purely mathematical. Have scrutinised Stephan's

links to actual
proofs of Cantor's theorem. But can one use the software to show that they

are indeed correct. This is the field of verification that I have interest in at this moment.

Can one find a tutorial about how specific mathematical proofs can be defined and verified ?

Thank you so very much

Marta

--

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/e7a7f648-facc-43cb-81e0-21b0f582ea05n%40googlegroups.com.

**Follow-Ups**:

**References**:**[tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs***From:*marta zhango

**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs***From:*'Martin' via tlaplus

- Prev by Date:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Next by Date:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Previous by thread:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Next by thread:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Index(es):