Chris, (01)
We seem to be talking at cross-purposes. (02)
Just to clarify a few points. (03)
> 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. (04)
But is this the only sense of complexity possible? Is the sense used in e.g.
complex systems (http://en.wikipedia.org/wiki/Complex_system) a part of
logic, or not about complexity? My guess is that not everyone reduces
complexity to logic. (05)
CP> > However, I did not see you making that argument.
CM> Yes, I see that you missed it.
I did notice the passage, but it seemed to me more a statement than an
argument. (06)
CM> 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. (07)
I cannot see where I (or John) made any claim like this. So not sure why
your comment is there. BTW I would expect people to avail themselves of
expressive power where they need it. (08)
OK, to save time. (09)
CM> 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. (010)
Agreed "theoretically possible". (011)
CM> 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). (012)
I assume there is a typo here, and it should read "ontologies will always be
built from tractable representational frameworks".
What I find odd is that you see this as "the only way". What I read John as
saying (and I tried to re-iterate) is that the IT community's experience to
date shows that there are a variety of practical strategies for managing
intractability. As your example of the travelling salesman shows, people
have found ways to deal with it that do not start by constraining the
representational framework. (013)
Maybe that is the bone of contention. You see a new Semantic Web problem and
tractable representational frameworks as "the only way" to solve it
unilaterally. Whereas I (and, I believe, John) see this as just one of a
series of common problems with a range of practical solutions that will
typically avoid confronting the problem. And we see the history of the last
50 years in computing as illustrating this. (014)
Regards,
Chris (015)
> -----Original Message-----
> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
> bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher Menzel
> Sent: 28 December 2009 18:34
> To: [ontolog-forum]
> Subject: Re: [ontolog-forum] blogic iswc keynote
>
> 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!),
>
> 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?
>
> > but whether the overall substance has any meat on it.
>
> Sorry, but I can't distinguish "meat" from "conclusion of a sound
> argument".
>
> > 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.)
>
> I have no idea why you consider it uncharitable to question the
> soundness of an argument.
>
> > 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.
>
> 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.
>
> > 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?
>
> > Interestingly the google test on "business systems intractability"
> gives results where intractability is about complexity rather than
> logic.
>
> 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.
>
> > Now maybe you can argue that business system practice is not
> relevant.
>
> I would never argue this.
>
> > That for KE on the semantic web we are (from a practical point of
> view) in a new situation.
>
> That is a very different point and my concern is that certain aspects
> of the vision of the Semantic Web *are* new.
>
> > 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.
>
> Yes, I see that you missed it. John wrote:
>
> >> 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.
>
> 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.
>
> > 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.
>
> Well, I thought it was clear enough the first time, but let me try
> again. Here, more explicitly, is the basic argument.
>
> 1. There is no restriction on the first-order statements one can use to
> build an ontology.
>
> 2. Consistency/validity/entailment are undecidable in first-order
> logic.
>
> 3. Therefore, it is possible that questions of
> consistency/validity/entailment will be undecidable on the Semantic
> Web.
>
> John's response is this:
>
> >> 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.
>
>
> 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.
>
> So, to keep things explicit, my argument above continues as follows:
>
> 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).
>
> 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.
>
> 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.
>
> 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).
>
>
> > My guess (and it is no more than a guess) is that while rules of
> inference (and so intractability) are part of the framework,
>
> ?? Rules of inference and intractability are entirely orthogonal
> notions.
>
> > 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.
>
> Indeed. I hope you find the argument more accessible now.
>
> Chris Menzel
>
>
> >> -----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
>
> _________________________________________________________________
> 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
> (016)
_________________________________________________________________
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 (017)
|