On 10/21/2011 1:55 AM, Figay Nicolas wrote:
> In expressive logics, size is less important than complexity. Euclid's
> Theorems don't make for a *large* KB, but good luck writing a reasoner
> that can return the rest of the Elements :) (01)
Most theorems that human mathematicians discover are easy to prove
with a modern theorem prover. The really hard part is to discover
what definitions are useful and what hypotheses are sufficiently
interesting to try proving. (02)
For his PhD dissertation in 1976, Doug Lenat developed the "Automated
Mathematician" (AM), which would hypothesize new theorems and try to
prove them. However, it generated huge numbers of trivial theorems. (03)
The hardest thing for AM to do was to "invent" interesting definitions
and hypotheses. If some human fed it a list of definitions and
statements of theorems, it could generate proofs quite easily.
But without a list of interesting definitions, AM would aimlessly
generate trivial theorems. (04)
In fact, Hao Wang wrote a theorem prover that proved all 378 theorems
in FOL and propositional logic that Whitehead and Russell had proved
in the _Principia Mathematica_. He did that in the late 1950s on
the IBM 704 -- a vacuum tube machine with 144K bytes of RAM -- and
it took a total of 7 minutes of CPU time for all 378 theorems. (05)
The elapsed time considerably much longer, because the 704 did not
overlap I/O and computation. Most of the time was spent in printing
the output. See (06)
Wang, Hao (January 1960). "Toward Mechanical Mathematics" (PDF). IBM
Journal of Research and Development 4 (1): 2–22. doi:10.1147/rd.41.0002. (07)
John (08)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (09)
|