Hi John, (01)
Quoting "John F. Sowa" <sowa@xxxxxxxxxxx>: (02)
> Michael et al.,
>
> The paper is nice, but 42 pages is more than twice the space needed
> to define the those terms. You can shorten it to much less than 20
> pages with a huge improvement in clarity, generality, and readability. (03)
You'd be surprised how long a paper gets when one has to provide proofs for all
of one's claims. (04)
>
> The key generalization that cuts through the muck is something I've
> been talking about for years: The Lindenbaum Lattice for a given
> logic and vocabulary. (05)
Although the Lindenbaum lattice is a nice abstraction, COLORE is a real system
that we are describing. The last third of the paper is about the procedures
that are used to decompose an ontology into modules and to update the
repository with new ontologies. The Lindenbaum lattice alone does not do this. (06)
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. (07)
>
> 6. Define the Lindenbaum lattice as the lattice of theories
> with entailment as the partial ordering.
>
> 7. Define a hierarchy as a finite subset of the Lindenbaum lattice. (08)
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).
 (09)
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. (010)
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. All of the relationships between
theories that are defined in the paper are required to do this. (011)
>
> Furthermore, once you introduce the Lindenbaum lattice, you can
> define all kinds of transformations and relationships among
> ontologies and their theories as walks through the lattice:
>
> 1. The AGM operators for belief revision (expand, contract,
> and revise) specify walks through the lattice: expand
> moves down, contract moves up, and revise moves sideways.
>
> 2. Deduction stays within a given theory. If the logic is
> complete, it can be used to derive any statement in the
> theory from any equivalent ontology.
>
> 3. Induction is a revision by expansion that can reduce the
> number of axioms by deriving generalizations. It may
> enlarge the theory to a proper superset, but it does
> not increase the size of the vocabulary.
>
> 4. Abduction is a revision by expansion that can also reduce
> the number of axioms, but it introduces new vocabulary
> and axioms that are not generalizations of statements
> in the theory. (012)
John, I have never seen you give any of these ideas any sort of formal
definition in the context of an ontology repository. Within COLORE, one could
consider some aspects of your very informal notion of abduction to be
formalized by the notions of definable interpretation, faithful interpretation,
and definable equivalence, all of which are well-understood within mathematical
logic. (013)
Also, the notion of reducibility (that we use as one of the fundamental
relationships for organizing the repository and supporting ontology
verification) does not seem to be covered by your informal relationships
above.
 (014)
>
> 5. All versions of nonmonotonic reasoning can be defined
> as similar walks through the lattice. This requires
> more discussion that would go beyond 20 pages. But it
> shows the power that come with the Lindenbaum L.
> (015)
It would be great to see you state the definitions of your ideas formally enough
to actually derive theorems and corollaries. (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)
|