SUO: Re: Conformance
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
AP = Adam Pease
JA = Jon Awbrey
PH = Pat Hayes
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.
JA: How are we to warrant that
the standard we put forward
is in conformity with itself?
AP: That is covered by [#3]. If the ontology contained
| p
| -p
a contraction would be derived by any first-order logic theorem prover.
JA: 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.
AP: 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.
JA: Okay, but it's not my problem --
it's yours if you chose to define
standard conformance in that way.
PH: 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.
PH: 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.
PH: 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.
PH: There are several things that need to be corrected here.
PH: 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.
PH: 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.
PH: 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.
PH: 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?
Thanks, Pat, for the update on PropSat, which is the
one nut's'helluva kingdomain that I have been trying
to keep up on all these years. Just to remind folks,
the question in question was about the tractability
of checking consistency in large FOL KB's. When it
comes to that, Pat, you have, as usual, managed to
conform all of my worst anxieties.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤