Re: A Single Foundational Logic for the Semantic Web

> 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