SUO: Re: inferencing relevance of the IFF (was: Re: Re: SUMO motion, and merging)
Robert,
Many thanks for the answer. I respect what you're trying to achieve,
but I'm unclear how it meets the goals of our charter. Our charter doesn't
address ontology mapping or translation. IFF seems like a product that
might help one compose ontologies in order to create a proposed standard
for the SUO, but that it is not a relevant proposal itself.
In terms of John's proposal for a combined effort, I could similarly see
IFF being used in combining SUMO, Cyc, or other ontologies, but the
resulting artifact would be the proposal to SUO, not the original
ontologies or IFF.
An additional concern that I have is that the utility, as opposed to the
mathematical possibility, of employing IFF to that end is also unsupported
by any examples or practical experience, at least so far as messages to
this mailing list are concerned. There are many folks working on ontology
mapping. What evidence is there that a category theory approach allows one
to merge ontologies faster, or more easily than other approaches, including
that of emacs and a human ontologist with no other tools?
Do you disagree with this line of reasoning?
Adam
At 11:42 AM 4/28/2003 -0700, Robert E. Kent wrote:
>John, Adam and others,
>
>On behalf of the IFF developers, here is a reply to the request for IFF
>inferencing relevance.
>
>Robert E. Kent
>rekent@ontologos.org
>
>
>----- Original Message -----
>From: "John F. Sowa" <sowa@bestweb.net>
>To: "Adam Pease" <apease@ks.teknowledge.com>
>Cc: <standard-upper-ontology@ieee.org>
>Sent: Monday, April 21, 2003 10:02 AM
>Subject: SUO: Re: SUMO motion, and merging
>
>
>[snip]
>
> > I extracted the following two conditions from your
> > note, which I agree with and which I believe should
> > be addressed in the joint motion:
> >
> > > Without at least one formal proof of IFF supporting
> > > a useful inference, I don't see the value in its inclusion.
> >
> > > Without the rules being released for Cyc and language
> > > definition addressed, I don't think it's a suitable proposal
> > > for SUO, nor would it add value to SUMO.
> >
> > I would ask the IFF and OpenCyc developers to comment on
> > these two points and to suggest ways in which they can be
> > addressed in the joint proposal.
>
>The IFF is a framework for object-level ontologies. In this sense it is
>content-free. Hence, the "useful inference" that you request support for
>cannot be directly about any content of the kind that SUMO or CYC provides.
>In fact, IFF complements SUMO in this regard, with IFF supporting inferences
>in Category Theory (CT), Formal Concept Analysis (FCA), and Information Flow
>(IF) that can be used to apply to _any_ content, for example, the kind that
>SUMO or CYC supplies.
>
>The IFF (with possibly extensions to its base-line axiomatisations) can
>support inferences for the usual theorems in the theories of CT,
>FCA and IF. These could be simple, such as the CT theorems that "all limits
>for a diagram are isomorphic" and "the power set and inverse image function
>form a functor on sets and functions" or more complex and interesting
>theorems, such as the FCA basic theorem characterizing concept lattices.
>The basic theorem of the FCA is provable in the IFF in its full
>category-theoretic generality as a category equivalence between the category
>of classifications and the category of concept lattices.
>Some of these theorems are only indirectly relevant to the lattice of
>theories application of the IFF, and some are quite relevant. And the
>relevancy may not be apparent at first.
>
>For one example, one simple but important theorem for moving between concept
>lattices is the theorem that "the composition of infomorphisms is
>well-defined; that is, the composition of infomorphisms satisfies the
>fundamental property (of an infomorphism)". Why is this important to the
>lattice of theories? The answer is that the lattice of theories is
>parametric in the sense that there is a lattice of theories for every first
>order language, and the natural way to connect these various lattices of
>theories together is via concept lattice morphisms defined from language
>morphisms between the base languages. This is just one example -- there are
>many others.
>
>For another example, the basic theorem FCA is very important in the
>transformation on objects from the truth classification over a 1st order
>language to the truth concept lattice of theories over the 1st order
>language, and on morphisms from the truth infomorphisms over a 1st order
>language morphism (or more generally, a 1st order interpretation) to the
>truth concept lattice of theories morphisms over a 1st order language
>morphism (or 1st order interpretation).
>
>So, in summary, the kinds of inferences supported by the IFF do not deal
>directly with the kind of content provided by SUMO or CYC, but rather with
>the framework itself that provides for systematic metalevel techniques for
>manipulation of an open-ended number of different theories ("moving from one
>theory to another theory, and for mixing, matching, combining, and
>transforming theories to whatever form is appropriate for whatever problem
>anyone is trying to solve") within a lattice of theories, or more generally
>within the category of theories.