Chris, (01)
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!), but whether the overall substance
has any meat on it. (02)
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.) (03)
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. 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? (04)
Interestingly the google test on "business systems intractability" gives
results where intractability is about complexity rather than logic. (05)
Now maybe you can argue that business system practice is not relevant. That
for KE on the semantic web we are (from a practical point of view) in a new
situation. 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. (06)
However, I did not see you making that argument. 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. (07)
My guess is that business systems engineers have developed heuristics for a
range of problems where intractability gets bundled in with a large number
of other things and so is not singled out. This is not a new idea. Herbert
Simon (and design science) makes a similar point. Interestingly I saw from
the outside something similar in action a year or so ago when Hasok Chang
(http://www.amazon.co.uk/Inventing-Temperature-Measurement-Scientific-Philos
ophy/dp/0195171276 - who I have mentioned before) was explaining to
engineers at the Royal Institute of Engineers how scientists develop
temperature measurement techniques to avoid awkward complications. The
engineers did not get it as these awkward situations were 'standard' for
them - and the science was non-standard engineering - as they faced these
problems in real life. (08)
My guess (and it is no more than a guess) is that while rules of inference
(and so intractability) are part of the framework, 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. (09)
However, all of this still leaves room for you to argue that the KE/semantic
web framework is different. (010)
CM>> Seriously? Only professional mathematicians and logicians are capable
> of conceiving, say, the traveling salesman problem? (011)
Interesting that you chose this example. For Simon and his ilk, this is an
example par excellence of design, where the heuristics for getting a
solution work around a complex problem (which may be intractability or just
difficult) rather than worry about dealing with it. Where practice is driven
by economics rather than 'truth'. I guess they would argue this is the
difference between theory and practice. (012)
I think this needs some more explanation (and I do not have a good one yet)
so if you have the arguments/explanations that show it is practical to
tackle intractability more directly, I would be really interested.
Otherwise, I guess we have to accept this is something waiting for a good
explanation. (013)
Regards,
Chris (014)
> -----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
> (015)
_________________________________________________________________
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)
|