On Dec 27, 2009, at 3:29 PM, Chris Partridge wrote:
> Chris,
>
> I think there is quite an important point at stake here. The real issue seems
>to me not whether one can pick holes in the details of John's points (however
>much fun that is!), (01)
Perhaps picking holes in the details of arguments is your idea of fun, but I
myself have far more satisfying sources. As to why you characterize pointing
out weak points in an argument as "picking holes", I'm at a loss. You do
realize that a sound argument depends on the truth of all of its premises and
the soundness of all of its individual inferences, right? (02)
> but whether the overall substance has any meat on it. (03)
Sorry, but I can't distinguish "meat" from "conclusion of a sound argument". (04)
> That is why if I were to accept, for the sake of this argument, your
>dissection of the points below, then I would feel you still do not get us to
>quite where you would want us to be. That something relevant has been missed
>out. (And that you have not been charitable enough to John.) (05)
I have no idea why you consider it uncharitable to question the soundness of an
argument. (06)
> I assume it is a relatively un-contentious point that most business system
>building practitioners would be surprised to hear that (logical)
>intractability is anything other than a theoretical problem when building
>systems. (07)
Perhaps because they are using logical frameworks where intractability is not
an issue? As John pointed out, reasoning in an RDB enables one to reason
relative to a fixed finite model and hence in polynomial time. (08)
> Many of the IT architects, designers and programmers I know would not even
>recognise the term. (If anyone disagrees, please let us know.) So how come
>they miss such an obvious problem? Maybe, at a practical level it is not a
>genuine category of problem? (09)
> Interestingly the google test on "business systems intractability" gives
>results where intractability is about complexity rather than logic. (010)
You appear to be confused about either complexity or logic. Complexity *is* a
part of logic, specifically, the theory of computability, which, along with
proof theory, model theory, and set theory, is one of the four branches
typically considered to be encompassed by modern mathematical logic. (011)
> Now maybe you can argue that business system practice is not relevant. (012)
I would never argue this. (013)
> That for KE on the semantic web we are (from a practical point of view) in a
>new situation. (014)
That is a very different point and my concern is that certain aspects of the
vision of the Semantic Web *are* new. (015)
> And you can see that in this situation (unlike with business systems)
>intractability becomes a problem. Maybe that is the way the argument should go.
>
> However, I did not see you making that argument. (016)
Yes, I see that you missed it. John wrote: (017)
>> 6. Check whether a given statement is true of all possible models -- prove a
>theorem.
>> ...
>>
>> Point #6 happens to be a very high priority among logicians who think that
>the primary use of logic is to form the foundation for mathematics. (018)
I replied: "John, I know this is one of your favorite hobby horses, but
irrespective of its importance to logicians, point #6 is surely a (not THE,
just A) critical component in the overall vision of the semantic web, as
already illustrated in points 1 and 2 above. If I am going to draw on your
knowledge base, I will want to know that your information is consistent with
mine and I will want to be able to calculate the implications of doing so."
And such calculations, of course, are undecidable in general. (019)
> And when/if you do, it would need to be a strong enough to give practical
>reasons why the heuristics that have grown up over the last half century when
>building business systems cannot be applied successfully in some way to the
>semantic web. I suppose this would involve an explanation of why the two are
>so different. (020)
Well, I thought it was clear enough the first time, but let me try again.
Here, more explicitly, is the basic argument. (021)
1. There is no restriction on the first-order statements one can use to build
an ontology. (022)
2. Consistency/validity/entailment are undecidable in first-order logic. (023)
3. Therefore, it is possible that questions of consistency/validity/entailment
will be undecidable on the Semantic Web. (024)
John's response is this: (025)
>> I acknowledge that some theorem proving is important. But please note that
>the Semantic Web consists primarily of RDF data -- i.e., a large volume of
>ground level assertions of the same logical nature as the tables of an RDB. (026)
I find this answer unsatisfying. If I'm understanding John correctly, he is
saying that the Semantic Web *as it exists now* is tractable, because it
consists primarily of ground RDF assertions and entailment for RDF restricted
to such assertions is tractable. (That is correct, IIRC.) But is this also
the vision for the *future* of the Semantic Web? To keep it uncontroversial,
my conclusion in the argument above is only that it is theoretically possible
that undecidability arise as a genuine issue on the Semantic Web. But there are
*already* interesting ontologies (e.g., PSL) that make robust use of the
expressibility of full first-order logic and hence that far exceed the
expressibility of RDF. And it seems to me exceedingly likely that the number
and importance of such ontologies will only grow as ontologists become more
familiar with the expressiveness of first-order logic and, concomitantly, come
to realize the serious expressive limitations of RDF. (Ironically, even
consistency/validity/entailment in full RDF are NP-complete -- are we to
believe that future ontologies on the Semantic Web won't even avail themselves
of *that*?) Moreover, there will not in general be some specific fixed, finite
model that one can reason with respect to. One might simply want to know
whether ontology A is consistent with ontology B; or whether statement S
follows from ontology C, independent of any fixed models. (027)
So, to keep things explicit, my argument above continues as follows: (028)
4. More and more ontologies on the Semantic Web will be expressed in full
first-order logic (or, at least, frameworks in which questions of
consistency/validity/entailment are, in general, intractable). (029)
5. Therefore, it is *likely* that issues of tractability will be a significant
problem that has to be confronted in the development of the Semantic Web. (030)
Perhaps I'm just naive here, but it seems to me that to assume that future
ontologies will not avail themselves of the full expressive power of FOL -- or
even simply the full power of decidable (but, in general, intractable)
frameworks like OWL-DL and unrestricted RDF -- is about as visionary as Bill
Gates' oft-quoted (apocryphal?) assertion that personal computers would never
need more than 64K of RAM. (031)
Please note: This is not a point of ideology for me. I'd be quite happy to
acknowledge that intractability is not a concern for the development of the
Semantic Web. I'd be happy to be convinced that the concerns above are
unwarranted. But it seems to me that the only way to show they are would be to
show that ontologies will always be built from in tractable representational
frameworks -- and that isn't even true *now* (nor -- and here John and I
completely agree -- would it be a good thing if it were). (032)
> My guess (and it is no more than a guess) is that while rules of inference
>(and so intractability) are part of the framework, (033)
?? Rules of inference and intractability are entirely orthogonal notions. (034)
> there are a number of other levels in the framework and all of these
>contribute to how practitioners address the problem. And it seems to me that
>when this is all in place practitioners have not found logical tractability a
>useful category (let me know if my sample is skewed). Now maybe they should,
>but that requires an argument that shows their current stance is not optimal. (035)
Indeed. I hope you find the argument more accessible now. (036)
Chris Menzel (037)
>> -----Original Message-----
>> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
>> bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher Menzel
>> Sent: 23 December 2009 18:47
>> To: [ontolog-forum]
>> Subject: Re: [ontolog-forum] blogic iswc keynote
>>
>> On Dec 18, 2009, at 1:32 PM, "John F. Sowa" <sowa@xxxxxxxxxxx> wrote:
>>> I was talking about the many different ways of using a statement in
>>> a logic, such as FOL. Theorem proving is only one use among many.
>>> In fact, it is probably very far down the list of things one might
>>> want to do with logic. For example,
>>>
>>> 1. Communicate some information -- i.e., transmit an assertion.
>>
>> Whose implications for your own knowledge base you might well want to
>> calculate. Calculating implications is just theorem proving.
>>
>>> 2. Check whether somebody's assertion is consistent with the
>>> facts -- i.e., evaluate truth in terms of a specific model.
>>
>> But in order to be consistent with the facts a statement must be
>> consistent simpliciter and the problem of consistency simpliciter is
>> undecidable. Hence, so too is the question of whether a statement is
>> consistent with the facts. Consistency checking, of course, is just
>> another name for theorem proving.
>>
>> So far your list is illustrating my point.
>>
>>> 6. Check whether a given statement is true of all possible models
>>> -- prove a theorem.
>>
>> Well, that's kind of a misleading way of putting it, since it is
>> impossible actually to check all possible models (as you well know).
>> Rather we (in effect) look for a proof and if we find one, then, of
>> course, it *follows* in virtue of soundness that the statement is true
>> in all possible models.
>>
>>> Point #6 happens to be a very high priority among logicians who think
>> that the primary use of logic is to form the foundation for
>> mathematics.
>>
>> John, I know this is one of your favorite hobby horses, but
>> irrespective of its importance to logicians, point #6 is surely a (not
>> THE, just A) critical component in the overall vision of the semantic
>> web, as already illustrated in points 1 and 2 above. If I am going to
>> draw on your knowledge base, I will want to know that your information
>> is consistent with mine and I will want to be able to calculate the
>> implications of doing so.
>>
>>>>> JFS> The paternalistic approach assumes that all users are trying
>> to prove a theorem that is valid for all possible models. But most
>> people who ask a question are only interested in a specific model,such
>> as the current DB.
>>>
>>>> CM> This isn't clear to me at all. If I'm just trying to describe a
>> certain conceptual domain like, say, human physiology...
>>>
>>> First of all, physiology is an experimental science. In the
>> development of that science, the most important use for any kind of
>> precise notation (say ordinary language expressed in a way that could
>> be translated to FOL) is to state observations and form
>> generalizations. That is communication (#1 on the list above), fact
>> checking (#2), and induction (#3).
>>>
>>>> CM> ... it doesn't seem to me that any inferencing is done vis-á-vis
>> any sort of fixed finite model.
>>>
>>> I have no idea what kind of inferencing you are talking about.
>> Physiologists aren't the kind of people who state anything in axioms.
>>
>> Then I have no idea what *you* are talking about. Of course
>> physiologists don't state things in terms of axioms. Isn't that
>> exactly the job of an ontologist? Isn't the whole idea here to get
>> such information represented formally in terms of a first-order
>> representation language?
>>
>>> They are much more likely to be doing #1, #2, #3, #4, and #5 above
>> than #6.
>>
>> At least two of which, as noted, entail #6.
>>
>>> Even physicists state in a tone of derision that they "don't do
>> axioms" -- that is in response to things like von Neumann'saxioms of
>> quantum mechanics.
>>
>> And ontologists don't "do" cloud chamber experiments. How is this
>> relevant? Of course physicists "don't do axioms". They are doing
>> physics; they are not trying to implement the Semantic Web.
>> Ontologists are, so they "do" axioms.
>>
>>> CM> which, if expressed in full FOL, raises the possibility of
>> intractability.
>>>
>>> That possibility is only slightly more likely than the chance that
>> the world will end tomorrow.
>>
>> Huh? You're saying that every "real world" problem is solvable in
>> polynomial time?
>>
>>> Nobody but a professional mathematician or logician is even capable
>> of "thinking" of an intractable statement, let alone worrying about
>> whether it can be proved.
>>
>> Seriously? Only professional mathematicians and logicians are capable
>> of conceiving, say, the traveling salesman problem? You really don't
>> think that's a real problem for, say, people working in logistics? And
>> are you really unaware of the problems of intractability in
>> computational biology or molecular dynamics (e.g., protein folding)?
>> How about n-body problems in physics and astronomy?
>>
>>> Please note that mathematicians have been using FOL for millennia.
>>> They were blissfully unaware of computational complexity or
>>> undecidability. Yet it never caused the slightest problem for them.
>>
>> Well, of course -- those problems didn't *exist*. There was no formal
>> model of computation prior to Turing, and no computers with which to
>> try to solve mathematically formulable problems, so there were no
>> mathematical problems of complexity and undecidability. But now there
>> are.
>>
>>> All the FOL statements that Whitehead and Russell stated in the
>> _Principia Mathamtica_ can be proved in a fraction of a second with
>> modern theorem provers.
>>
>> I am frequently amazed at how fast Prover9 and its ilk are able to
>> solve problems involving multiply-nested quantifiers -- more so because
>> I had once programmed a tree-based theorem prover on my own as a
>> programming exercise that was mostly miserable at solving such
>> problems. However, this is really neither here nor there. W&R were
>> not interested in problems that give rise to intractability. All of
>> their theorems are highly amenable to automated solution (obviously).
>>
>>> CM> I'm not saying [intractability] can't be managed -- obviously, it
>> can, if only by putting temporal bounds on searches for proofs and
>> countermodels. But that there might be a need to do so if one uses full
>> FOL does need to be expressed.
>>>
>>> Yes, such checks should be part of the development methodology.
>>
>> Really? Why? I thought intractability is just a concern for
>> professional mathematicians, logicians and other out of touch ivory-
>> tower denizens?
>>
>> I agree with you on most matters, John, but your views on
>> intractability mystify me.
>>
>> -chris (038)
_________________________________________________________________
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 (039)
|