ontolog-forum
[Top] [All Lists]

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

 To: "[ontolog-forum]" "John F. Sowa" Wed, 23 Dec 2009 15:11:16 -0500 <4B327964.8000403@xxxxxxxxxxx>
 ```Chris,    (01) A relational database can be viewed as either a theory consisting of a conjunction of ground level assertions (without negations) or as a specification of a model (a collection of individuals and relations over them).    (02) If you view an RDB as a theory, then you are doing theorem proving. But if you view it as a model, then you are doing metalevel operations of transforming one model into another. Either way, the operations on ground level clauses with no negations are very fast.    (03) JFS>> Theorem proving is only one use [of logic] 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.    (04) CM> Whose implications for your own knowledge base you might well want > to calculate. Calculating implications is just theorem proving.    (05) Or it could be considered model manipulation. One of the most important kinds of model-theoretic operations is to evaluate the denotation of a proposition in terms of a model. That is not normally considered theorem proving.    (06) JFS>> 2. Check whether somebody's assertion is consistent with the >> facts -- i.e., evaluate truth in terms of a specific model.    (07) CM> But in order to be consistent with the facts a statement must be > consistent simpliciter and the problem of consistency simpliciter is > undecidable.    (08) Please note that I was talking about "a specific model". To evaluate the truth or falsity of an FOL statement in terms of a Tarski-style model is not only eminently decidable, it can be done in polynomial time in the *worst* case. If the DB is indexed (as most are), many common queries can be evaluated in linear or even logarithmic time.    (09) CM> Consistency checking, of course, is just another name for theorem > proving.    (010) But in the case of an RDB, it is more fruitful to think of it as equivalent to evaluating Tarski's evaluation function for a single model.    (011) I keep citing the following paper. Please read it:    (012) http://www.jfsowa.com/pubs/fflogic.pdf Fads and Fallacies about Logic    (013) Both Pat Hayes and Jim Hendler liked it. I think that you would probably like it if you had read it.    (014) JFS>> 6. Check whether a given statement is true of all possible models >> -- prove a theorem.    (015) CM> 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.    (016) Look at what I wrote on the second line "-- prove a theorem." I made the point that you elaborated.    (017) JFS>> 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) CM> ... 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.    (019) 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.    (020) The information that is exchanged through RDF or DB updates consists of ground level clauses. Each update is usually checked for consistency by a Tarski-style evaluation of "database constraints" -- i.e., FOL statements or axioms -- in terms of those clauses. That takes polynomial time in the worst case, and linear or logarithmic time in the most common cases.    (021) The problem of aligning the ontologies of two different DBs is a much more difficult issue -- because there you really do have to do some theorem proving with full FOL. In some cases, that can get into intractable issues. But in many cases, there is a clever way out:    (022) A theory T is consistent iff it has a model.    (023) For many practical systems, we don't have to look for models. The models are there: it's the content of all the ground level clauses in the RDF or RDB. If we want to know whether two theories are consistent on all possible models, we have to do theorem proving. But frequently, we can get away with checking whether they are consistent with the current model -- and that's polynomial time.    (024) JFS>> 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.    (025) CM> 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?    (026) You are confirming what I just said. Those are people who have taken graduate-level courses in mathematics. It's irrelevant whether their job code says mathematician or computational biologist. They're doing the same kind of things.    (027) But please note that the set of people who have taken graduate level courses in mathematics *and* use that knowledge in their daily jobs are a tiny fraction of one percent of the population. Those aren't the people who need a paternalistic system that protects them from themselves. In fact, they probably use tools such as Mathematica, which lets them do some very sophisticated kinds of things.    (028) CM> I agree with you on most matters, John, but your views on > intractability mystify me.    (029) I think that we are focusing on different kinds of problems. If we actually sat down and itemized the applications we're thinking of, we'd find that we agree what level of computation is required in each case.    (030) Please look at the KR at Cyc. They use a superset of FOL, and they seldom, if ever, found that the expressive power caused any problems with intractability. They did have problems with performance, but that is the result of data management issues with a large amount of stuff to be organized and pushed around.    (031) Look at the work by Bill Andersen & Co., which I cite in the fflogic.pdf paper. They analyzed the Cyc axioms, and found that the overwhelming majority of them can be mapped into efficiently computable Horn-clause rules. The ones that required full FOL could be used as database constraints, which are evaluated in polynomial time when the updates are performed.    (032) John    (033) _________________________________________________________________ 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    (034) ```
 Current Thread Re: [ontolog-forum] blogic iswc keynote, (continued) 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 Re: [ontolog-forum] blogic iswc keynote, John F. Sowa