Very useful link. Thanks.

 

-Matthias

 

Von: Ben Goertzel [mailto:[EMAIL PROTECTED] 
Gesendet: Mittwoch, 22. Oktober 2008 15:40
An: agi@v2.listbox.com
Betreff: [agi] A huge amount of math now in standard first-order predicate
logic format!

 


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 |  <https://www.listbox.com/member/archive/303/=now> Archives
<https://www.listbox.com/member/archive/rss/303/> |
<https://www.listbox.com/member/?&;
7> Modify Your Subscription

 <http://www.listbox.com> 

 




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

Reply via email to