Hello John, (01)
John Sowa wrote:
>
> But for the next edition, I would recommend a much
> shorter and simpler paper that starts with the Lindenbaum lattice
> and AGM. Anything else is defined in those terms, and the finite
> hierarchies are treated as starting subsets that can be enlarged
> as needed.
>
> John
> (02)
You still don't quite see some of the underlying motivations and functionalities
for COLORE. (03)
*All* possible first-order theories are in the Lindenbaum lattice,
so of course hierarchies and repositories are suborderings.
".. starts with the Lindenbaum lattice" is really equivalent to
saying that you using first-order theories -- there is nothing more
to the Lindenbaum lattice than that.
This is why the Lindenbaum lattice alone is too coarse to serve as the sole
notion for organizing the repository. The additional relationships we use are
needed for practical applications of ontology repositories.
On the other hand, I still claim that your proposal to use AGM is too
imprecise to support the applications that we need -- ontology verification and
modularization. (04)
1. Hierarchies (sets of theories with the same signature) are the building
blocks for the repository. (05)
The root theory of a hierarchy captures the fundamental ontological
commitments for the domain. For example, all timepoint ontologies are
definably equivalent to semilinear orderings; there are no timepoint
ontologies within the literature or used in practice which are
definably equivalent to arbitrary partial orderings. This property
is reflected in the axioms of the root theory in the Timepoint hierarchy. (06)
Trunk theories are not arbitrary theories, but rather
reflect the possible design choices for ontologies in
a particular domain (e.g. time, mereology, ...). (07)
Note that the hierarchy is only a semilattice because in general there
will be inconsistent sets of design choices. (08)
The other feature of hierarchies, and which is not true for arbitrary
suborderings of the Lindenbaum lattice, is that
we can use the same translation definitions for all theories in the
same hierarchy when specifying interpretations between theories. (09)
2. The relationships between theories in different hierarchies are
required for ontology verification (which is the characterization of
the mdoels of the ontology up to elementary equivalence). (010)
3. Ontologies are decomposed into modules through the notion of
reducibility (which is not a metatheoretic relationship that is part
of the definition of the Lindenbaum lattice). (011)
A module of an ontology is then an axiomatization of a subtheory of the
ontology. One can take an “internal" view of modules in the sense that
an ontology is explicitly constructed by extending and combining existing
ontologies in the repository. An alternative “external" view decomposes
an ontology based on logical relationships of its subtheories
to existing modules in the repository. (012)
Each module is a subtheory that is definably equivalent to a theory that
belongs to a unique hierarchy. Again, without the notion of hierarchy,
this distinction would be lost. (013)
4. We need to update the repository with a new theory and then identify
how it is related to other theories in the repository (not its relationship
to all other first-order theories typed by monkeys on typewriters).
The Procedures at the end of the paper focus on this notion of update.
We propose semi-automated procedures for the decomposition and refinement of
ontologies that rely on the existing modules in the repository,
giving **practical** guidance for modularizing ontologies and designing new
modular ontologies. (014)
If we consider trunk theories in a hierarchy and core theories
within the reduction of a theory to be the building blocks of ontologies,
then the number of such modules is bounded by the number of axioms within
the theory. Of course, this can lead to an exponential set of theories in
the repository if we explicitly construct all possible combinations of
trunk theories and core theories.
We investigate a series of procedures which decompose any ontology
into a set of core theories, and which identify the set of trunk theories
which are equivalent to a core theory. The only theories that we require
to explicitly be included within the repository
are those required by core hierarchies being closed and atomistic. (015)
5. The meet of two theories in the Lindenbaum lattice does not
capture all of the intuitions for the similarity of two theories.
See Section 2.2 of the paper for more detailed discussions. (016)
- michael (017)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (018)
|