- From: Sandro Hawke <sandro@w3.org>
- Date: Thu, 18 Apr 2002 15:48:05 -0400
- To: msabin@interx.com
- cc: www-rdf-logic@w3.org
> Sandro Hawke wrote, > > In other words, if you can get a machine to do something with > > logic X, then you can, in essense, get every machine which > > understands Horn clauses (or Java, or whatever) to do the same > > thing with logic X. If you can't get a machine to handle logic > > X, you're really out of luck in any case. > > This is true, but unfortunately not very useful. > > I can't remember the details, but in his paper, "A Curious > Inference", the late George Boolos gives an example of a proof > which is trivial in second order system, and which can be proved in > first order systems, but only in a completely infeasible number of > moves. > > More generally, it's not just _what_ can be proved which is > affected by the expressivness of your underlying logic, but also > what can be proved _practically_. Are you saying that using Horn clauses for programming instead of something like Java bytecode will have an unacceptable performance cost? If so, I counter that Horn clauses have better modularity and mobility characteristics, and in the vast majority of computer applications, those are more important areas to optimize.... But that's all subject to debate in picking a Turing-equivalent logic. Java bytecode or WAM bytecode or any of hundred other candidates, some being hybrids..... I think you're raising a different spectre: there's some logic with an effective decision procedure where the procedure is still not really useful. Maybe that's true, but I don't see it as a problem. If you have a computer program that runs on your computer and does good things with your logic, then the Church-Turing Thesis pretty much backs me up in saying we can make it run anywhere (give or take some performance issues, but see previous paragraph). If you can't make it run on your computer, you shouldn't be thinking it will somehow run on the Semantic Web. -- sandro
Received on Thursday, 18 April 2002 15:51:43 UTC