Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautolo... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		gone35 on Jan 29, 2015 \| parent \| context \| favorite \| on: A Computer Scientist Tells Mathematicians How to W... 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 on Jan 29, 2015 [–]

For the Isabelle theorem prover I know the Archive of Formal Proofs [0].

[0] http://afp.sourceforge.net/

gone35 on Jan 30, 2015 | [–]

Damn; 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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact