Tuesday, February 21, 2006
The Second School of Semantic Science
ontologyMapping Glass Bead Games
On the limits of the OWL standard à [184]
Reading material [1]
Reading material [2]
Reading material [3]
Summary of the discussion up to this point à [186]
Regarding machine theorem provers
Communication from Paul Werbos
Though I don't have time (or skills?) for it myself, I still tend to believe that machine-verified theorems and proofs are a very important area of un-met opportunity.
Many theorems have proliferated in many areas that are hard to prove because they are not true. Also, theorems are inherently translatable to multiple languages. And, yes, one could find some application for automated provers or proof-assistants in such a context.
Alex Zenkin, among others, has shown great interest in this area -- even though his own ideas about the continuum hypothesis do suggest there might be some interesting challenges in specifying alternative standards of proof -- axioms -- that users should have access to.
I was intrigued the other day to read a book on very practical differential equations and control theory (by Larry Evans maybe, Springer for sure) which said "the status of these theorems depends on what kind of set theory you start from..."
But it's not my core area...
Best of luck,
Paul Werbos