On Tue, Jul 24, 2012 at 6:41 AM, Bill Richter <[email protected]> wrote: > But I do it now only for Mizar, and I told you the results (the > shortening would be about 1400 lines of your Mizar code to some 300, > if ATPs could prove everything). > > Josef, that's great, and Mizar is fine. Can you show me your 300 lines of > Mizar code,
Just remove all the toplevel proof ... end blocks in your original Mizar article. > and tell me how to run it on Vampire? I did: click the red/black icons in that html-ized version. For a longer story and Emacs access, read http://arxiv.org/pdf/1109.0616 . Best, Josef (I am probably not doing email in the next two weeks) ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
