Dick, (01)
RHM> Not wanting to drop context, my "2. group 3" propositions
> include the philosophy that propositions are created by humans. (02)
Nobody asked you to drop context, and nobody denies that propositions
are created by humans. My only suggestion was that if you want mKR
to be useful, you need to give a clear, formal definition of its
syntax and semantics. (03)
As an example of the level that had been achieved 50 years ago,
I have often recommended the following article: (04)
Wang, Hao (1960) Toward mechanical mathematics,
_IBM Journal of Research and Development_ 4, pp. 2-22. (05)
In 1959, Hao Wang wrote a program for the IBM 704 (a vacuum machine
computer with 144K bytes of RAM) that proved all the propositions
stated in both propositional logic and first-order logic in the
first 3 chapters of the _Principia Mathematica_. (06)
Since then, people have implemented theorem provers that have gone
far beyond that level on machines that are many thousands of times
larger and faster than the IBM 704. I recommend the TPTP web site
for "Thousands of Problems for Theorem Provers": (07)
http://www.tptp.org (08)
Wang had a PhD in philosophy from Harvard, but in his paper, he did
not spout "philosophy that propositions are created by humans."
Instead, he focused on the syntax, semantics, rules of inference,
and his method for implementing them. (09)
The people who designed systems to prove the TPTP problems did
the same. Their web site provides a large number of useful tools,
the documentation for using them, and thousands of test cases.
Fortunately, they don't try to proselytize us with their philosophy. (010)
John (011)
_________________________________________________________________
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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (012)
|