Re: SUO: RE: conformance
Chris,
Good comments. How would you recommend that the conformance wording be
changed? The common sense notion I wanted it to incorporate was that uses
of SUO which included a definition which contradicted something in SUO
could not claim to be conforming. For example, if there were an axiom in
the SUO that requires subclasses of A and B to be disjoint it would not be
allowed to have some application that uses SUO, that claims to be
conforming, and yet defines a new term C as a subclass of both A and B.
Adam
At 11:43 AM 10/10/2001 -0500, Chris Menzel wrote:
>Adam wrote:
> > - 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.
>
>Adam,
>
>Best to scotch (3) here -- and not only because SUMO is "nearly"
>inconsistent as it stands (as I've pointed out at length in a previous
>message -- still to no avail, apparently). While I have argued
>vociferously for avoiding known contradictions, consistency per se
>shouldn't be a conformance criterion, as consistency is not decideable for
>ontologies that contain at least just a bit of elementary arithmetic.
>(This is Goedel's so-called second incompleteness theorem.)
>
>That said, it is often possible -- and generally a good thing -- to
>provide *relative* consistency proofs for ontologies. This typically
>consists of building a *model* of a given ontology in some set theory --
>ZF say. (The existence of a model for an ontology entails that it is
>consistent, by the soundness theorem for first-order logic.) A proof in
>ZF of the existence of such a model then shows that, *if* ZF is
>consistent, then your ontology is consistent as well. (The consistency of
>your ontology is thus "relative" to the consistency of ZF.) Even though
>we can't prove it, we've got pretty good reason to believe ZF is indeed
>consistent. Hence, a relative consistency proof for our ontology gives us
>good reason to believe that it is consistent as well. (As a side benefit,
>set theoretic models of our ontologies also often yield a great deal of
>insight into the structures that we intend our ontologies to describe
>-- Pat Hayes' work on temporal ontologies is a great example of this.)
>
>If we fail to find a model of our ontology, it of course doesn't follow
>that the theory is inconsistent -- we might just not be smart enough to
>find a model. However, unless an ontology is pretty complex, our
>inability to find a model gives us reason to question its consistency, and
>hence to give it a very close second look. (I'll bet you can't find a
>model of SUMO's current class theory, for example.) I would therefore
>include the search for relative consistency proofs in the *methodology* of
>ontology construction, but would not include the existence of such proofs
>as a conformance criterion.
>
>-chris
>
>--
>
> /\ ASCII ribbon | Chris Menzel -- http://philebus.tamu.edu/~cmenzel
> \/ campaign | Philosophy Dept, Texas A&M University
> /\ against | College Station, TX 77843-4237
>/ \ HTML email | voice: 979.845-5660 fax: 979.845.0458
Adam Pease
Teknowledge
(650) 424-0500 x571