4 ms·
Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to alr
by gone35 12y ago
Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to already-established proofs from some common repository? Maybe future versions of TLAPS would benefit from such a thing?
(Sorry if this already exists; I'm just an interested layman.)
- qznc 12y agoFor the Isabelle theorem prover I know the Archive of Formal Proofs [0]. [0] http://afp.sourceforge.net/ http://afp.sourceforge.net/
- gone35 12y agoDamn; this is amazing stuff... I had no idea: (from [1]) so just get a local copy, set the path, and voila you can import... Wonderful. Thank you for sharing this! http://afp.sourceforge.net/using.shtml http://afp.sourceforge.net/using.shtml