Re: SUO: Internal Consistency proof?
Pat,
A little "for-what-it's-worth" tangent, below.
At 08:41 2003-05-03, Patrick Cassidy wrote:
>Just a thought about the problem of internal consistency:
>
> Adam Pease mentioned in his discussion of experience with SUMO:
>
> > ... as well as being impossible in practice on theories of
> > any significant size, we have done proofs for consistency
> > within specified time boundaries. We found and removed
> > inconsistencies found in up to 50-step proofs. We can run
> > for days now without finding anything, so we have some
> > degree of confidence that SUMO is internally consistent.
>
> If the size and structure of some module or combination of
> modules of an ontology makes it impractical to prove internal
> consistency in days of computing, perhaps that task can be designed,
> like the SETI screen saver, to run in the background and parts of the
> task distributed to willing ontologists to get as much confidence as
> possible in any given ontology. ...
SETI@home is going to transition from it's current purpose-built
software to "BOINC" (the Berkeley Open Infrastructure for Computing), a
generic framework for such distributed computing projects. See
<http://boinc.berkeley.edu/> for more information.
I have not looked into it and don't know what constitute the
indications and contraindications for applications suitable to its
facilities, but I suppose it's not beyond the realm of possibility that
it could be put to use in truth maintenance and KB or ontology
consistency checking. However, as a rule, this kind of distributed
computing depends on problems that can be decomposed into sub-tasks
that require little or no interaction with each other. SETI's signal
processing is very well-suited to this requirement. I'm inclined to
think that theorem proving and other logic-based computation is less
well-suited in this respect. It's possibly also a contraindication to
have to distribute full KBs to the participants unless the KB is rather
modest in size or changes very infrequently.
Nonetheless, the tools are there to explore this option. (BOINC is not
the only one, either, but I'm even less familiar with the others--look
for "grid computing" on Google to find them).
>... It is understood that each new axiom would require another round
>of computing, but for any given proposed SUO, our group might in this
>way find some probabilistic confidence measure for the logical
>consistency, though not the utility, of a proposed standard. Would
>creating such a background consistency-checker be an appropriate task
>for someone involved in the SUO? I myself am clueless as to how to do
>it. But I would be willing to retire my SETI screen saver and let my
>machine run consistency proofs on any proposed standard. Does this
>make any sense?
>
> Pat
Randall Schulz