[Tlaplus-users] Induction

Maniatis, Petros petros.maniatis at intel.com
Mar 6 Juil 18:10:50 CEST 2010


Hello everyone,

 

Are general inductive proofs possible within tlaps? I know that isabelle
supports things like induct and the nat-induct rule, but I was wondering if
anyone has a suggestion on how to structure induction proofs for TLA+ to
avoid making them back-end-specific.

 

Thanks.

 

Petros

 

------
Petros Maniatis

Research Scientist
Intel Labs Berkeley 

 

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/tlaplus-users/attachments/20100706/0e0d5752/attachment.htm>
-------------- section suivante --------------
Une pièce jointe autre que texte a été nettoyée...
Nom: smime.p7s
Type: application/x-pkcs7-signature
Taille: 7151 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/tlaplus-users/attachments/20100706/0e0d5752/attachment.bin>


More information about the Tlaplus-users mailing list