Michael, (01)
I think that a failure to discuss the use cases is a cause
of the misunderstanding: (02)
> You still don't quite see some of the underlying motivations
> and functionalities for COLORE. (03)
Let me jump to your point #4, which is almost identical to what
I have been saying in writings and email notes since 1999: (04)
> 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. (05)
I completely agree with that point. (06)
The AGM operators (plus relabeling) specify how to relate any theory
in the lattice to any other. If you emphasize implemented theories
(which I agree are the most important ones to consider), you may need
to pass through other theories in the lattice that are not the ones
you have in your hierarchy of implemented theories. (07)
But you never have to relate the theories you are primarily working
with to the totality of all those that exist only in that great
Platonic heaven. (08)
> 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. (09)
I agree. I would never consider or construct more than I need. (010)
> 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. (011)
I believe that the procedures I proposed are equivalent to yours,
but with different terminology. Some fundamental principles: (012)
1. The three AGM operators are contraction, expansion, and revision.
Expansion adds a proposition, contraction deletes a proposition,
and revision is a contraction followed by an expansion. Contraction
always produces a more general theory, and expansion produces a
more specialized theory. (013)
2. The propositions that are added or deleted are not necessarily
axioms. (Note that many different axiomatizations may have
exactly the same theory as their closure.) (014)
3. Point #2 implies that deleting an axiom is not sufficient for
contraction if the axioms are not independent. And if the
proposition is not an axiom, the problem is a bit more
complicated. The AGM literature covers these issues. (015)
4. Point #2 also implies that adding a proposition to the axioms
might not change a theory if the proposition is already implied
by the other axioms. The AGM lit also covers this issue. (016)
5. Expansion can create a contradiction if the new proposition
added to a theory happens to be false in that theory. That
requires a theorem prover to check for possible contradictions.
In some cases, that step can be undecidable. But there are
many important cases in which it is decidable and efficient. (017)
6. Any theory in the lattice can be converted to any other by
(a) deleting all axioms from the first, and (b) adding all
axioms from the second. But we'd prefer to relate them by
minimal changes, if possible. That issue is also discussed
in the AGM literature. (018)
7. One way to reduce the number of steps is by the operation
of "interpreting" one theory in terms of another. I prefer
to call that a combination of relabeling the vocabulary
(i.e., signature) in conjunction with other revision operators. (019)
Since repeated use of these operations can relate (or transform) any
theory to any other, all the operations you define can be defined in
terms of them. The intuitive metaphor I use is "walking through the
lattice". Every step in this walk is precisely defined. The problems
that can be encountered have also been thoroughly analyzed and methods
for handling them have been proposed and implemented for AGM. (020)
Some other points: (021)
> 1. Hierarchies (sets of theories with the same signature) are the building
> blocks for the repository. (022)
You've got that in the LL. For every signature V, there is a lattice
of theories with that signature, and it is a sublattice of the big one. (023)
> 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. (024)
That's an example of an important sublattice in the LL. (025)
> Trunk theories are not arbitrary theories, but rather
> reflect the possible design choices for ontologies in
> a particular domain (e.g. time, mereology, ...). (026)
We are in complete agreement on this point. (027)
> 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). (028)
Complete agreement, except for your use of the word 'hierarchy'
instead of lattice. (029)
> 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. (030)
Total agreement. (031)
> 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. (032)
Loss of agreement. What distinction? As opposed to what? (033)
In any case, I believe that everything you want to define can be
defined by talking about lattices for the theory, and relating
them to implemented (or specified) theories in the hierarchies. (034)
But I'll be traveling for the holidays, starting tomorrow.
So I will be out of touch with my email for a while. (035)
John (036)
_________________________________________________________________
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 (037)
|