Re: SUO: a silly question about the new modular architecture
Seth, Adam, et al.,
I believe that those requirements are quite reasonable. That is very
much like the kind of environment I would like to see as well.
> Yes. I don't really believe in a standard ontology (woops ... sorry for the
> heresy). But at the same time I want an ontology that I don't have to
> construct myself. I like to pick and choose.
I agree, but with some change of wording. I believe that what we need
is a collection of basic modules that contain theories for all the major
top-level categories (e.g., space, time, space-time (3 & 4 D),
mathematics
(sets, collections, partial orderings, lattices, numbers, etc.), plants,
animals, people, geography, money, actions (walk, run, jump, eat, drink,
buy, sell, etc.), organizations, languages, communication, etc.
And there should be a framework of high-level categories which provide
the pigeonholes for storing, finding, and organizing all those theories.
But there should be options for different theories that go into
different levels of details with different perspectives on the same
basic categories.
> I believe that the most
> useful SUMO would have a front end tool where the ~user~ answers a set of
> questions and clicks on a set of contexts .. the tool would then generate
> the needed ontology. Then where certain axioms were still unacceptable, one
> could replace them individually ... the tool would then thread through the
> selected knowledge and delete any contradictions and suggest where new
> axioms were needed.
There are already very good off-the-shelf tools for doing those kinds
of things. As an example, there are very theorem provers for FOL that
can be used to check whether a collection of axioms is consistent.
For many theories, those tools can prove consistency in a few seconds
of CPU time. For others, they may require several minutes. But they
might also run into undecidable theories for which consistency cannot
be guaranteed.
For most purposes, undecidability is not a problem. Whenever the
theorem prover fails to verify a theory overnight, the probability
that the theory is wrong or inconsistent is very high, and the
kn. engineers should take a very hard look to see what's wrong.
And by the way, exactly the same tools can be used with either
small modules or a single giant monolith. The only difference is
that the small modules are easier to verify than a single big
theory.
Bottom line: Most of the tools that would be needed to implement
a lattice of theories would be just as valuable (if not more so)
for a single monolithic theory. The lattice does not need anything
extra -- it just makes things easier for humans (and computers) to
verify, test, and understand.
John Sowa