Re: SUO: Re: Conformance
>¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>
>Adam,
>
>Okay, but it's not my problem --
>it's yours if you chose to define
>standard conformance in that way.
>
>Jon
>
>¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>
>Adam Pease wrote:
>>
>> Jon,
>> Computational complexity isn't my area I'm afraid. Pat or Chris Menzel
>> might be able to give you some good pointers. In general though, although
>> tractable inference and completeness are desirable, in my opinion, they're
>> neither necessary nor strictly possible for the content we have. Basically,
>> you may not be able to catch all problems but you can be pretty sure.
>>
I would say that completeness is necessary, at least in some sense
(though I would agree that it needs to be stated very carefully), but
that for the SUO, complexity should not be a major concern. However,
that said, there is no doubt that most standards work in this area is
overwhelmingly dominated by complexity issues, so the likelihood is
very high that the potential user community is going to demand some
sensitivity to these issues. For example, it would be good to have
some syntactic characterization of which parts (modules?) of the SUO
could be paraphrased in a description-logic framework like DAML+OIL,
and which could not.
As a general point, I think it is important that the SUO, like any
standards effort, takes into account the likely needs of its intended
user community. I have seen very little in the way of any discussions
about who is likely to make use of the SUO, or any effort to contact
any of them for their views. A standard that is used only by its
authors may give them a feeling of authenticity, but that hardly
seems sufficient to justify all the work involved.
> > Adam
>>
>> At 07:24 PM 10/9/2001 -0400, you wrote:
>> >¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>> >
>> >Adam,
>> >
>> >If you could post any current literature citations on
>> >the computational complexity of consistency checking for
>> >up-&-runniing theorem provers on large knowledge bases,
>> >it might help to alleviate some anxieties on this score,
>> >as the last time I was following these developments the
>> >picture wasn't too pretty, but that was ten years ago.
>> >
There are many more recent results. Purely propositional
satisfiability detection has a worst-case complexity of something
like N. k|v where v is the number of propositional variables, N is a
small polynomial in n, the number of clauses, and k is about 1.5 (it
keeps changing slightly.) Most of the effort in quantifier logics has
been in describing subcases which have provably tractable (
polynomial) decision problems, which is what description logics are
all about. These are now both pretty expressive and also startlingly
efficient; look at Ian Horrocks' work, for example. Personally the
work I find most interesting is the probabilistic analyses of large
propositional spaces, where one finds again and again that the
complexity of the satisfiability problem depends on the v/n ratio,
and for almost all values, the answer is trivial; the odds of the
clause set being satisfiable are either overwhelmingly high (when n/v
is small) or overwhelmingly low (when n/v is large), with a narrow
'critical region' - which has been identified fairly precisely, I
gather - where the satisfiability problem has a high average
complexity. So although there are some high peaks in the central
region, most of the complexity landscape is virtually flat; a very
encouraging result. Markov planners that take advantage of this
phenomenon are able to handle clause sets measured in 6 or 7 figures
with ease; Lucent has done a lot of work in this area.
> > >Thanks,
>> >
>> >Jon
>> >
>> >¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>> >
>> >Adam Pease wrote:
>> > >
>> > > Jon,
>> > > That is covered by [#3]. If the ontology contained
>> > >
>> > > p
>> > > -p
>> > >
>> > > a contraction would be derived by any first-order logic theorem prover.
> > > >
>> > > Adam
>> > >
>> > > At 01:38 PM 10/9/2001 -0400, you wrote:
>> > >
>> > > >¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>> > > >
>> > > > AP = Adam Pease
>> > > >
>> > > > AP: - Implementations of SUO are "ontologies" or
>>"information models".
>> > > > - A conforming implementation is an ontology or
>>information model that:
>> > > > [#1] Uses terms as defined by the SUO, or
>> > > > [#2] Uses terms that are defined (using SUO-KIF)
>> > > > entirely by other terms in the SUO
>> > > > [#3] Is consistent: a contradiction cannot be derived by means
>> > > > of first-order logic from the set of statements belonging
>> > > > to the implementation and the SUO.
> > > > >
There are several things that need to be corrected here. First, it
obviously isn't appropriate to insist that conformance requires using
ONLY terms from the SUO. After all, it is only supposed to be an
UPPER ontology, not the whole thing. Conformance should require
rather that all (?) terms 'fit underneath' terms from the SUO, maybe;
but that would need to be made precise.
Second, the notion of 'being defined' needs to be spelled out more
exactly, particularly as (the last time I looked) SUO-KIF doesn't
have any syntactic provision for stating definitions.
Third, why the consistency condition? This seems to me to be quite
inappropriate for a conformance clause. Part of the business of the
conforming engine might be to detect inconsistencies, for example.
(If inconsistencies are nonconforming, then that job is trivial,
since there can't be any , by definition..) Also this places an
uncomputable burden on any conformance tester; the problem even of
detecting conformance isn't decideable.
Fourth, this entire approach to conformance seems to be only
concerned with namespaces, and ignores the axioms and the logical
language used. Suppose someone writes a block of DAML and uses the
SUO namespace: does that constitute conformance? Or must what they
say about the named concepts also conform to the SUO axioms? How is
*that* kind of conformance specified? Must they use SUO-KIF?
Pat Hayes
--
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes