SUO: Certification. Was "Motion for a joint SUO project (extended)"
Pat,
Thanks for the support:
> I think that John Sowa's motion makes a lot of
> sense, but I would like to see it extended, since
> it does come close to what I think would be a
> method for creating a truly functional upper
> ontology drawing on the CYC, SUMO, and potentially
> other existing upper ontologies as well as newly
> added content. Most importantly, it provides a
> mechanism for inclusion of viewpoints not yet much
> discussed on this list, nor submitted as candidate
> ontologies.
But I'm renaming this thread "Certification" because
the issue of consistency is both complex and central
to the question of how any particular ontology (or
module of an ontology) is certified and approved.
Following are some points to keep in mind:
1. Proving consistency of an arbitrary collection
of axioms is not always possible. It may be
undecidable -- i.e., the theorem prover will
run forever without reaching a conclusion.
2. However, there are many important theories
that are quite easy to prove consistent
with just an ordinary theorem prover.
3. But there is a way to prove consistency
even without a theorem prover: demonstrate
that there exists at least one model (i.e.,
at least one example) for which the axioms
are true. If so, then they are guaranteed
to be consistent.
4. Of course, finding a model for an arbitrary
set of axioms is, in general, just as hard as
using a theorem prover to prove consistency.
But for ontologies, there is a golden lining:
since ontologies are supposed to be true of
something that exists, the people who are
designing the ontology should always have at
least one example in mind. If you check each
axiom against the examples as you go along,
then you can be sure that you are preserving
consistency. Examples for an ontologist
correspond to test cases for a programmer.
5. But if you have a very large ontology, such
as Cyc (or even SUMO), it is very hard to
find examples that are rich enough to test
all the aspects of all the microtheories.
Therefore, the smaller microtheories that
deal with more limited aspects of the
ontology are more likely to be consistent
than a large ontology, such as Cyc or SUMO.
I would add two additional points (4 and 5). The
revised motion is immediately below, and John's
previous motion is below that. I also added one
word to John's point number 3, highlighted by
asterisks, to avoid the ambiguity that was
contained in one of my previous comments.
I also modified the referent of the "more
specialized" phrase in point 3.
Point 4 is added so that, even if proof of
full consistency is not possible, at least some
effort would be made to detect inconsistency,
and some measure of probability of consistency
between modules is generated. Users should have
some confidence that mixing and matching specific
modules will not cause obvious consistency problems.
The word "pairwise" might be changed to include
combinations of more than two modules, especially
where a "Base Ontology" top module is combined
with two lower-level modules.
Point 5 is added so that potential users can
be assured that they will not have to use all of
the pieces of a module in order to use that
part of it that would be needed in their own
application. I think this could help increase
the pool of potential users. Whether this is
of practical importance depends on how large a
module is. Some modules could be rather large,
but a selection mechanism would mitigate the
inhibitions a potential user might feel when
modules containing elements important in one
application also include a lot of unnecessary
content. It is not necessary that development of
such a selection utility be started immediately, but
I think it is worthwhile to consider it as an
essential component of a standard that is
intended to be widely used.
In accepting this motion, the participants from
Cycorp or Teknowledge need not feel obliged to
slow down their existing work, but would agree to
make some effort to respond to queries, especially
about possible additions to their own ontologies or
possible changes that might make their individual
ontologies more consistent with others.
Pat
=============================================
Patrick Cassidy
MICRA, Inc. || (908) 561-3416
735 Belvidere Ave. || (908) 668-5252 (if no answer)
Plainfield, NJ 07062-2054 || (908) 668-5904 (fax)
internet: cassidy@micra.com
=============================================
===========================
Suggested Substitute Motion
===========================
___________________________________________________
Should the IEEE P1600.1 Standard Upper Ontology
Working Group commence work on a project to develop
a standard based on three starting candidates,
IFF, OpenCyc, and SUMO, and continuing as follows:
(1) The development process shall include a
collaboration of members of all three groups
and other SUO participants to determine how each
of the three starting candidates can complement
and support the contributions of the others.
(2) The results shall include a library of modules
derived from OpenCyc, SUMO, and/or other sources.
Each module shall consist of closely related
axioms and definitions for some aspect of a
standard upper ontology.
(3) The standard shall include the specification
of methodologies for testing the modules for
**internal** consistency; relating them to one another
in a generalization/specialization hierarchy;
and combining two or more modules to derive a
new module that is larger than the individual
component modules and more specialized than the
full set of modules from which it was drawn.
(4) The standard shall include the specification
of a methodology for testing for logical consistency
between the modules, providing an incomplete
and partial test where full consistency cannot
be proven due to time constraints.
(5) The standard shall include the specification of
a method for extracting from any set of pairwise
logically consistent (i. e. not proven to be logically
inconsistent) modules, a subset of the classes,
relations, functions, and axioms that are sufficient
as a basis for creating an application domain
ontology.
===========================
John Sowa's motion
===========================
John F. Sowa wrote:
>
> After all the discussion with Adam, John D, and
> others, I have revised my draft motion in the
> statement at the end of this note.
>
> The new statement makes it clear that SUMO,
> OpenCyc, and IFF are all starting candidates
> on an equal footing. It emphasizes that the
> developers collaborate to determine how their
> work can complement the work of the others.
> But it doesn't say how much, if any, of the
> three starting projects and documents should
> end up in the final standard.
>
> Point #3 replaces the word "lattice" with the
> term "generalization hierarchy". I would assume
> that the infinite lattice and/or other related
> mathematical structures would be part of the
> theory underlying the methodology. But the
> library of modules would only be a finite subset.
> Every lattice of theories is a generalization
> hierarchy, but a finite excerpt from a lattice
> need not be a lattice.
>
> The methodology mentioned in Point #3 is far
> less than what is contained in the IFF document.
> It is what I would consider the barest minimum
> that should be extracted from IFF to support
> the development and use of the modules. I
> would leave it up to the development process
> to determine how much more of IFF should be
> incorporated in the methodology.
>
> Perhaps there could be two resulting documents:
> an IEEE Technical Report that presents the full
> IFF theory, and a much smaller specification
> in the standard of just those operators that
> are actually used in the methodology.
>
> I hereby move that the following question should
> be put to a vote of the SUO Working Group.
>
> John Sowa
> ___________________________________________________
>
> Should the IEEE P1600.1 Standard Upper Ontology
> Working Group commence work on a project to develop
> a standard based on three starting candidates,
> IFF, OpenCyc, and SUMO, and continuing as follows:
>
> (1) The development process shall include a
> collaboration of members of all three groups
> and other SUO participants to determine how each
> of the three starting candidates can complement
> and support the contributions of the others.
>
> (2) The results shall include a library of modules
> derived from OpenCyc, SUMO, and/or other sources.
> Each module shall consist of closely related
> axioms and definitions for some aspect of a
> standard upper ontology.
>
> (3) The standard shall include the specification
> of a methodology for testing the modules for
> consistency, relating them to one another in
> a generalization/specialization hierarchy,
> and combining two or more modules to derive a
> new module that is larger and more specialized
> than the modules from which it was derived.
>
--