Michael, (01)
> You'd be surprised how long a paper gets when one has
> to provide proofs for all of one's claims. (02)
Exactly! That's why it's important to build on work that
has already been done instead of starting from scratch. (03)
> Although the Lindenbaum lattice is a nice abstraction,
> COLORE is a real system that we are describing. (04)
Yes, indeed. The Lindenbaum Lattice is *pure theory*. It is not
an implementation, but it applies to any implementation that is
based on a logic L, a vocabulary V, and an entailment relation |=. (05)
If T1 |= T2, then T2 is a generalization of T1, and T1 is a
specialization of T2. We can use the less-than-or-equal
symbol <= for |=, and less-than < for proper generalization.
(Specialization is =>, and proper specialization is >.) (06)
My claim: the Lindenbaum Lattice provides the basic framework
for the COLORE system. There are other things you may want say
and prove about COLORE. But they're much easier to state, prove,
teach, and understand when you define them in terms of the lattice. (07)
> For example, consider the notion of the similarity of theories within the same
> hierarchy. Intuitively, this is the strongest shared subtheory of two
>theories,
> but the formal definition is complicated by the fact that this is not
> equivalent to finding a common subset of axioms. (08)
This is an excellent example of how the lattice simplifies and clarifies
the specifications. The definition is trivial: your "strongest shared
subtheory" of two theories is their supremum (AKA maximal common
generalization). That is the ideal definition: it's precise, formal,
short, and sweet. According to the theory, the supremum always exists,
but the theory of lattices does *not* say how to compute it. (09)
If you want to compute the supremum, then you need more detail.
The best place to find that detail is in the huge literature about
belief revision. The AGM axioms (expand, contract, and revise)
specify the ways of moving up, down, and sideways through the
lattice. They give lots of theorems, proofs, and algorithms. (010)
I cite the AGM axioms whenever I talk about the lattice. For
a textbook, you're expected to repeat the details, but a citation
is sufficient in a research paper. (011)
> Simply invoking the Lindenbaum lattice is too simplistic. Entailment does not
> distinguish between conservative and nonconservative extension, both of which
> are essential relationships for understanding different approaches to ontology
> modularity. The notion of a hierarchy (set of theories with the same signature
> and ordered by nonconservative extension) is not clearly distinguished from
> other subsets of theories by entailment within the Lindenbaum lattice. This is
> not to say that it can't be distinguished, but it does require the definitions
> of additional relations beyond entailment (and which are not addressed by your
> relations below). (012)
As I said, the lattice doesn't cover everything you might want to say,
but it covers a lot. In this case, every extension is a specialization.
The terms conservative and nonconservative can be defined as in Def 3
in your paper. (013)
> One of the primary themes of the paper is the relationship between ontology
> repositories and different approaches to modularity -- decomposing an ontology
> into smaller subtheories. We use the motion of reducibility to identify a set
> of theories in the repository whose union is definably equivalent to the
> ontology that we are analyzing. A subtheory of the ontology that are definably
> equivalent to one of these repository theories constitutes a module within the
> ontology. It is difficult to see how any of your relationships below can be
> used in this way. (014)
Given any set of theories A1, A2, ... An, the infimum of all of them
is their minimal common specialization. (015)
In the discussion of hierarchies, you should also note that there is
a sublattice for any subset V1 of the vocabulary V of the big lattice, (016)
Another operator I add to the AGM operators is *relabeling* (in my KR
book, I called it analogy, but the term _relabeling_ avoids confusion).
For any theory of modularity, you want to add the option of taking
any module (theory or sublattice) and relabel some or all the names.
This gives you another theory (or sublattice) that is located in
another part of the big lattice and can be combined with other
theories that use the same vocabulary. (017)
> We have used reducibility and COLORE to verify OWL-Time and the time
>ontologies
> in Pat Hayes' Catalog of Temporal Theories. We are currently using it to
>verify
> shape ontologies and process ontologies... (018)
That's fine. But you can define everything in terms of the lattice and
simplify a lot of the discussion and proofs. (019)
> John, I have never seen you give any of these ideas any sort of formal
> definition in the context of an ontology repository. (020)
Please look in any textbook about lattices. That's the foundation.
For more recent work, especially on computational details, look at
the literature on belief revision. (021)
JFS
>> All versions of nonmonotonic reasoning can be defined
>> as similar walks through the lattice. (022)
> It would be great to see you state the definitions of your ideas formally
> enough to actually derive theorems and corollaries. (023)
The literature on lattices and the literature on belief revision cover
nearly everything I've been talking about. I also discussed these
issues in Sections 6.4 and 6.5 of my KR book with exercises at the
end of Chapter 6 that apply the techniques. (024)
In any case, I am currently writing a textbook _Principles of Logic
and Ontology_, in which I'll provide more detail. (025)
John (026)
_________________________________________________________________
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 (027)
|