I had not noticed this before, though it was posted earlier this year. Finally Josef Urban translated Mizar into a standard first-order logic format:
http://www.cs.miami.edu/~tptp/MizarTPTP/<http://www.cs.miami.edu/%7Etptp/MizarTPTP/> Note that there are hyperlinks pointing to the TPTP-ized proofs of each theorem. This is math with **no steps left out of the proofs** ... everything included ... This should be a great resource for AI systems that want to learn about math by reading definitions/theorems/proofs without needing to grok English language or diagrams... Translating this TPTP format into something easily loadable into OpenCog, for example, would not be a big trick Doing useful inference on the data, on the other hand, is another story ;-) To try this in OpenCog, we gotta wait for Joel to finish porting the backward-chainer from NM to OpenCog ... and then, dealing with all this data would be a mighty test of adaptive inference control ;-O ben g -- Ben Goertzel, PhD CEO, Novamente LLC and Biomind LLC Director of Research, SIAI [EMAIL PROTECTED] "A human being should be able to change a diaper, plan an invasion, butcher a hog, conn a ship, design a building, write a sonnet, balance accounts, build a wall, set a bone, comfort the dying, take orders, give orders, cooperate, act alone, solve equations, analyze a new problem, pitch manure, program a computer, cook a tasty meal, fight efficiently, die gallantly. Specialization is for insects." -- Robert Heinlein ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
