Re: SUO: Question
Bob,
That's an important issue that I would explain in more detail
in a tutorial about the complete system, but I'll give a brief
summary here:
> In your proposal of an (infinite) lattice of all possible theories, do
> modules that are ill formed also fit into this lattice (e.g. do not
> have any stated or consistent methodology, are defective or
> inappropriate in some other way)? I assume so since it is all
> possible theories" even poorly formed or simply false theories.
Yes, the infinite lattice has an infinite amount of room for all that
is good, bad, or indifferent. The lattice does in fact make provision
for theories that are inconsistent (i.e., imply p and not-p for some p).
By the usual rules of first-order logic, any and every statement of any
kind is provable from such a contradiction. That means that all such
theories collapse into a special theory at the bottom of the lattice,
which is commonly called the "absurd" theory. That theory corresponds
to a general trash bin for all the inconsistent theories.
However, the formalism, by itself, does not distinguish "good"
theories from "bad" theories based on methodology or suitability
for any particular application. Those features would be determined
by various metalevel criteria: the amount of testing, the methodology
used to derive it, the level of validation or certification, etc.
Those characteristics should accompany each module in the lattice.
> If both SUMO and OpenCyc were in the lattice would they be considered
> as a single module or broken down into component modules? Would the
> component modules be considered a single theory or would they be
> evaluated on the basis of the individual theories that compose the
> component modules?
Both SUMO and OpenCyc were developed from collections of much smaller
theories and modules. Ian Niles put together many modules that were
taken from different sources in constructing SUMO, and he sometimes
had to modify them in order to make them fit. I would like to see
those modules broken out so that users could evaluate their quality
based on their source, revision history, and amount of testing and use.
Modules for the basic mathematical functions, for example, are much
more likely to be carefully constructed and tested than theories for
some topic that is still a matter of debate.
> Could the individual theories be recombined to form new modules?
Yes, that is one of the major advantages of a lattice. The operators
on a lattice (which can be defined in terms of Boolean operations on
the axioms of the theories) determine the most specific generalization
(the supremum) of any two theories or the most general specialization
(the infinimum) of any two theories. Those are the kinds of operators
that are informally computed by merging the axioms of the component
modules into a big ontology, such as SUMO or Cyc. But the definition
of the lattice spells out the details of how it's done.
The advantage of the lattice is that it allows the user to choose
only the minimal number of modules that are needed for a particular
application. Bill Andersen developed techniques for extracting axioms
from Cyc in order to use them in a different inference engine. But
if the complete ontology were already organized in a lattice of modules,
the selection could be done in a systematic way without requiring all
the efforts that Bill had to exert in order to do the extraction.
> Assuming one has an method of evaluation, how does one chose among a
> number of acceptable modules? A standard should be appropriate and
> used for most purposes (85 - 90%).
In Bill's application, he took the set of axioms that were specifically
written for the particular application and traced the chains of
definitions to determine which ones were defined in terms of which
other predicates, which in turn were defined in terms of which other
predicates all the way back to the top.
But if the theories were already organized in a lattice, the chains
of dependencies would be shown explicitly: Any particular theory
would depend on all the more general theories that occurred above
it in the hierarchy -- i.e., the partial ordering of the lattice.
There beauty of the lattice of theories is that you can define
it in one page. But you could write an entire book to explain all
the useful implications that come out of that one page. There is
very little that has to be implemented, but you get a lot of
"bang for the buck" out of it.
John Sowa