Chris, (01)
CM> As to why you characterize pointing out weak points in an argument
> as "picking holes"... (02)
I *always* appreciate corrections to any errors in my arguments, but
in that particular note that I sent there weren't any "weak points".
(I'm including a copy of my response to your earlier note below.) (03)
What I was objecting to is the repetition of unqualified statements
like the following, which you just repeated in the most recent note: (04)
CM> 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. (05)
Qualifications: (06)
1. Every major programming language in use today is undecidable
in the sense that there can be no general proof that a program
written in it will terminate. (07)
2. But no programmer would ever dream of asking for a less
expressive language. (08)
3. For all kinds of computation, including the Semantic Web
and relational databases, there is a question that is vastly
more important than undecidability or even intractability
-- namely, *efficiency* . (09)
4. Decidability is usually defined as computable in finite time,
and tractable is defined as computable in polynomial time.
But when you have millions or billions of data items, any
polynomial with an exponent greater than 1 is a disaster. (010)
5. If you want an answer within your lifetime, the difference between
a thousand years, a billion years, or forever is irrelevant. (011)
I agree that computational complexity is important for both logic
and programming. But we must make it clear that reducing the
expressive power of a language can *never* solve any problem.
It merely makes certain problems impossible to state. (012)
John (013)
-------- Original Message --------
Subject: Re: [ontolog-forum] blogic iswc keynote
Date: Wed, 23 Dec 2009 15:11:16 -0500
From: John F. Sowa (014)
Chris, (015)
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). (016)
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. (017)
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. (018)
CM> Whose implications for your own knowledge base you might well want
> to calculate. Calculating implications is just theorem proving. (019)
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. (020)
JFS>> 2. Check whether somebody's assertion is consistent with the
>> facts -- i.e., evaluate truth in terms of a specific model. (021)
CM> But in order to be consistent with the facts a statement must be
> consistent simpliciter and the problem of consistency simpliciter is
> undecidable. (022)
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. (023)
CM> Consistency checking, of course, is just another name for theorem
> proving. (024)
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. (025)
I keep citing the following paper. Please read it: (026)
http://www.jfsowa.com/pubs/fflogic.pdf
Fads and Fallacies about Logic (027)
Both Pat Hayes and Jim Hendler liked it. I think that you would
probably like it if you had read it. (028)
JFS>> 6. Check whether a given statement is true of all possible models
>> -- prove a theorem. (029)
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. (030)
Look at what I wrote on the second line "-- prove a theorem." I made
the point that you elaborated. (031)
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. (032)
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. (033)
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. (034)
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. (035)
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: (036)
A theory T is consistent iff it has a model. (037)
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. (038)
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. (039)
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? (040)
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. (041)
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. (042)
CM> I agree with you on most matters, John, but your views on
> intractability mystify me. (043)
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. (044)
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. (045)
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. (046)
John (047)
_________________________________________________________________
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 (048)
|