Re: SUO: a silly question about the new modular architecture
John,
At 08:35 PM 8/31/2001 -0400, John F. Sowa wrote:
>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.
Could you provide a URL to code that one could download?
>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
Adam Pease
Teknowledge
(650) 424-0500 x571