ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] blogic iswc keynote

 To: "[ontolog-forum]" Christopher Menzel Wed, 23 Dec 2009 12:47:23 -0600 <5496A2ED-2F85-4AAF-910E-985048AAE894@xxxxxxxx>
 ```On Dec 18, 2009, at 1:32 PM, "John F. Sowa" 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.    (01) Whose implications for your own knowledge base you might well want to calculate. Calculating implications is just theorem proving.    (02) > 2. Check whether somebody's assertion is consistent with the > facts -- i.e., evaluate truth in terms of a specific model.    (03) 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.    (04) So far your list is illustrating my point.    (05) > 6. Check whether a given statement is true of all possible models > -- prove a theorem.    (06) 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.    (07) > 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.    (08) 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.    (09) >>> 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.    (010) 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?    (011) > They are much more likely to be doing #1, #2, #3, #4, and #5 above than #6.    (012) At least two of which, as noted, entail #6.    (013) > 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.    (014) 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.    (015) > 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.    (016) Huh? You're saying that every "real world" problem is solvable in polynomial time?    (017) > 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.    (018) 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?    (019) > 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.    (020) 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.    (021) > 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.    (022) 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).    (023) > 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.    (024) Really? Why? I thought intractability is just a concern for professional mathematicians, logicians and other out of touch ivory-tower denizens?    (025) I agree with you on most matters, John, but your views on intractability mystify me.    (026) -chris    (027) _________________________________________________________________ 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    (028) ```
 Current Thread Re: [ontolog-forum] blogic iswc keynote, (continued) Re: [ontolog-forum] blogic iswc keynote, Rick Murphy Re: [ontolog-forum] blogic iswc keynote, ravi sharma Re: [ontolog-forum] blogic iswc keynote, Ali Hashemi Re: [ontolog-forum] blogic iswc keynote, sowa Re: [ontolog-forum] blogic iswc keynote, sowa Re: [ontolog-forum] blogic iswc keynote, Rob Akscyn Re: [ontolog-forum] blogic iswc keynote, Christopher Menzel Re: [ontolog-forum] blogic iswc keynote, John F. Sowa Re: [ontolog-forum] blogic iswc keynote, Christopher Menzel Re: [ontolog-forum] blogic iswc keynote, John F. Sowa Re: [ontolog-forum] blogic iswc keynote, Christopher Menzel <= Re: [ontolog-forum] blogic iswc keynote, John F. Sowa Re: [ontolog-forum] blogic iswc keynote, Rich Cooper Re: [ontolog-forum] blogic iswc keynote, sowa Re: [ontolog-forum] blogic iswc keynote, Rich Cooper Re: [ontolog-forum] blogic iswc keynote, Chris Partridge Re: [ontolog-forum] blogic iswc keynote, Christopher Menzel Re: [ontolog-forum] blogic iswc keynote, Chris Partridge Re: [ontolog-forum] blogic iswc keynote, John F. Sowa Re: [ontolog-forum] blogic iswc keynote, Christopher Menzel Re: [ontolog-forum] blogic iswc keynote, Jim Rhyne